Theorem orc 400

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
orc	⊢ (𝜑 → (𝜑 ∨ 𝜓))

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 121	. 2 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))
2	1	orrd 393	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385

This theorem is referenced by:  pm1.4  401  orcd  407  orcs  409  pm2.45  412  pm2.67-2  417  biorfi  422  biorfiOLD  423  pm1.5  544  pm2.4  599  pm4.44  601  pm4.45  724  pm3.48  878  orabs  900  norbi  904  andi  911  pm4.72  920  biort  938  pm5.71  977  consensus  999  dedlema  1002  ifptru  1023  3mix1  1230  cad0  1556  cad11  1558  19.33  1812  19.33b  1813  dfsb2  2373  moor  2526  ssun1  3776  undif3OLD  3889  reuun1  3909  eqoreldifOLD  4226  opthpr  4384  disjord  4641  elelsuc  5797  ordelinelOLD  5826  ordssun  5827  fununmo  5933  tpres  6466  soxp  7290  omopth2  7664  swoord1  7773  swoord2  7774  sornom  9099  fin56  9215  fpwwe2lem12  9463  ltle  10126  nn1m1nn  11040  elnnz  11387  elnn0z  11390  zmulcl  11426  nn01to3  11781  ltpnf  11954  xrltle  11982  xrltne  11994  s3sndisj  13706  s3iunsndisj  13707  nn0o1gt2  15097  prm23lt5  15519  4sqlem17  15665  cshwsidrepswmod0  15801  cshwsdisj  15805  cshwshash  15811  funcres2c  16561  tsrlemax  17220  odlem1  17954  gexlem1  17994  drngmuleq0  18770  maducoeval2  20446  alexsubALTlem3  21853  dyadmbl  23368  bcmono  25002  gausslemma2dlem0f  25086  nb3grprlem1  26282  frgrwopreg  27187  frgrregorufr  27189  2wspmdisj  27201  frgrregord13  27254  dfon2lem4  31691  dfrdg4  32058  btwnconn1  32208  segcon2  32212  broutsideof2  32229  lineunray  32254  meran1  32410  dissym1  32420  bj-orim2  32541  bj-peircecurry  32545  bj-consensus  32562  bj-sbsb  32824  bj-unrab  32922  wl-orel12  33294  orfa  33881  tsor2  33955  lkrlspeqN  34458  fnwe2lem3  37622  ifpid1g  37839  ifpim3  37841  rp-fakeanorass  37858  or3or  38319  clsk1indlem3  38341  ntrclsk3  38368  19.33-2  38581  ax6e2ndeq  38775  uunT1  39007  undif3VD  39118  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  disjxp1  39238  salexct  40552  salexct3  40560  salgencntex  40561  salgensscntex  40562  otiunsndisjX  41298  nn0o1gt2ALTV  41605  odd2prm2  41627  ldepspr  42262  elfzolborelfzop1  42309  blen1b  42382  eximp-surprise2  42531