Theorem jaod 873

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))

Assertion

Ref	Expression
jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 33	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 33	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 871	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 33	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  mpjaod  874  orel2  904  pm2.621  912  pm2.63  955  jaao  969  jaodan  972  ecase3d  1050  dedlema  1061  dedlemb  1062  cad0  1651  psssstr  4058  eqoreldif  4646  opthpr  4811  prel12g  4824  opthprneg  4825  axpr  5389  sotric  5589  sotr2  5593  sotr3  5600  relop  5828  suctr  6452  trsucss  6454  ordelinel  6467  fununi  6616  fnprb  7215  soisoi  7337  ordunisuc2  7856  poxp  8141  soxp  8142  frrlem12  8316  frrlem13  8317  tfrlem11  8397  onelfvnef1  8450  omordi  8575  om00  8584  odi  8588  omeulem2  8592  oewordi  8601  nnmordi  8641  omsmolem  8667  swoord2  8752  nneneq  9222  dffi3  9424  inf3lem6  9635  cantnfle  9673  cantnflem1  9691  cantnflem2  9692  ttrcltr  9718  r1sdom  9782  r1ord3g  9787  rankxplim3  9899  carddom2  10059  wdomnumr  10144  alephordi  10154  alephdom  10161  cardaleph  10169  djuinf  10268  cfsuc  10336  cfsmolem  10349  sornom  10356  fin23lem25  10403  fin1a2lem11  10489  fin1a2s  10493  zorn2lem7  10581  ttukeylem5  10592  alephval2  10658  fpwwe2lem12  10728  gch2  10761  gchaclem  10764  prub  11080  sqgt0sr  11192  1re  11309  lelttr  11401  ltletr  11403  letr  11405  mul0or  11957  prodgt0  12165  mulge0b  12188  squeeze0  12221  sup2  12274  un0addcl  12640  un0mulcl  12641  nn0sub  12657  elnnz  12704  zindd  12801  rpneg  13155  xrlttri  13269  xrlelttr  13286  xrltletr  13287  xrletr  13288  qextlt  13334  qextle  13335  xmullem2  13396  xlemul1a  13419  xrsupexmnf  13436  xrinfmexpnf  13437  supxrun  13447  prunioo  13613  difreicc  13616  iccsplit  13617  uzsplit  13731  fzm1  13742  expcl2lem  14217  expeq0  14236  expnegz  14240  expaddz  14250  expmulz  14252  sqlecan  14354  facdiv  14432  facwordi  14434  bcpasc  14466  resqrex  15418  absexpz  15473  caubnd  15527  summo  15884  zsum  15885  zprod  16105  rpnnen2lem12  16394  ordvdsmul  16471  nn0rppwr  16736  nn0expgcd  16739  dvdsprime  16863  2mulprm  16869  ge2nprmge4  16878  prmdvdsexpr  16894  prmfac1  16897  pythagtriplem2  16996  4sqlem11  17134  vdwlem6  17165  vdwlem9  17168  vdwlem13  17172  cshwshashlem3  17276  prmlem0  17284  pleval2  18510  pltletr  18516  plelttr  18517  tsrlemax  18761  smndex1mgm  19107  f1omvdco2  19663  psgnunilem2  19710  efgredlemc  19960  frgpuptinv  19986  lt6abl  20110  dmdprdsplit2lem  20262  domneq0  20961  lvecvs0or  21387  unichnlidl  21517  baspartn  23273  0top  23302  indistopon  23320  restntr  23501  cnindis  23611  cmpfi  23727  filconn  24203  ufprim  24229  ufildr  24251  alexsubALTlem2  24368  alexsubALTlem3  24369  alexsubALTlem4  24370  ovolicc2lem3  25841  rolle  26311  dvivthlem1  26329  coeaddlem  26569  dgrco  26595  plymul0or  26600  aalioulem3  26662  cxpge0  27012  cxpmul2z  27020  cxpcn3lem  27076  scvxcvx  27314  sqf11  27467  ppiublem1  27530  lgsdir2lem2  27654  lgsqrlem2  27675  2sqnn0  27766  2sqnn  27767  fltoprmgt3  27997  nosepon  28023  nolesgn2ores  28030  nogesgn1ores  28032  nosepne  28038  nolt02o  28053  nosupbnd1lem5  28070  madebdaylemlrcut  28286  madebday  28287  ltslpss  28295  addsproplem2  28357  leadds1  28376  addsuniflem  28388  mulsproplem9  28511  sltmuls1  28534  sltmuls2  28535  muls0ord  28572  precsexlem9  28602  precsexlem11  28604  recsex  28606  abssnid  28630  ltonold  28648  onnolt  28653  eucliddivs  28763  elnnzs  28788  expsne0  28823  bdaypw2n0bndlem  28850  bdayfinbndlem1  28854  z12zsodd  28869  lmieu  29290  upgrpredgv  29718  edglnl  29722  eucrct2eupth  30847  frgrogt3nreg  30999  nvmul0or  31253  hvmul0or  31628  snsssng  33111  disjxpin  33183  expgt0b  33409  axprALT2  35735  subfacp1lem4  35949  satfvsucsuc  36131  satfrnmapom  36136  sat1el2xp  36145  gonarlem  36160  gonar  36161  goalrlem  36162  goalr  36163  fmlasucdisj  36165  satffunlem1lem1  36168  satffunlem2lem1  36170  untsucf  36476  dfon2lem6  36551  broutsideof2  36888  btwnoutside  36891  broutsideof3  36892  outsideoftr  36895  lineunray  36913  lineelsb2  36914  nmuladdss  36963  ltnadd  36968  nadddilem4  36973  finminlem  37107  nn0prpw  37112  refssfne  37147  meran1  37200  ontgval  37220  ordcmp  37236  axtcond  37267  bj-sngltag  37897  bj-axseprep  37991  bj-prmoore  38037  topdifinfindis  38271  icoreclin  38282  rdgssun  38303  finxpsuclem  38322  poimirlem24  38564  poimirlem25  38565  poimirlem29  38569  poimirlem31  38571  mblfinlem2  38578  ovoliunnfl  38582  itg2addnclem  38591  sdclem2  38678  fdc  38681  divrngidl  38964  lkreqN  40229  cvrnbtwn4  40338  4atlem12  40671  elpaddn0  40859  paddasslem17  40895  paddidm  40900  pmapjoin  40911  llnexchb2  40928  dalawlem13  40942  dalawlem14  40943  dochkrshp4  42448  lcfl6  42559  lcmineqlem  43104  primrootspoweq0  43158  aks6d1c1  43168  sticksstones22  43220  aks6d1c6lem3  43224  oexpreposd  43381  expeqidd  43384  sn-remul0ord  43461  sn-sup2  43557  fphpdo  43825  pellfundex  43894  jm2.19lem4  44000  jm2.26a  44008  ordnexbtwnsuc  44270  onov0suclim  44277  oege2  44310  succlg  44331  dflim5  44332  oacl2g  44333  omcl2  44336  omcl3g  44337  naddgeoa  44397  safesnsupfiss  44417  fzunt  44457  fzuntd  44458  fzunt1d  44459  fzuntgd  44460  relexpmulg  44711  relexp01min  44714  relexpxpmin  44718  relexpaddss  44719  clsk1indlem3  45044  or2expropbi  48105  ich2exprop  48554  poprelb  48607  reuopreuprim  48609  goldbachthlem2  48632  nprmdvdsfacm1lem2  48707  nprmdvdsfacm1  48710  requad01  48720  evenltle  48816  gbowge7  48862  bgoldbtbndlem3  48906  elclnbgrelnbgr  48924  clnbgrel  48927  dfclnbgr6  48955  dfnbgr6  48956  dfsclnbgr6  48957  upgrimpths  49008  clnbgrgrim  49033  isubgr3stgrlem4  49068  isubgr3stgrlem7  49071  grlimgredgex  49099  gpgedgvtx1  49161  gpgvtxedg0  49162  gpgvtxedg1  49163  lidldomn1  49329  uzlidlring  49333  prelrrx2b  49827  line2y  49868  itschlc0xyqsol1  49879  itsclc0xyqsolr  49882  inlinecirc02plem  49899