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  1650  psssstr  4037  eqoreldif  4642  opthpr  4805  prel12g  4818  opthprneg  4819  axpr  5388  sotric  5588  sotr2  5592  sotr3  5599  relop  5827  suctr  6451  trsucss  6453  ordelinel  6466  fununi  6616  fnprb  7215  soisoi  7337  ordunisuc2  7856  poxp  8143  soxp  8144  frrlem12  8319  frrlem13  8320  tfrlem11  8400  onelfvnef1  8453  omordi  8578  om00  8587  odi  8591  omeulem2  8595  oewordi  8604  nnmordi  8644  omsmolem  8670  swoord2  8755  nneneq  9225  dffi3  9427  inf3lem6  9638  cantnfle  9676  cantnflem1  9694  cantnflem2  9695  ttrcltr  9721  r1sdom  9785  r1ord3g  9790  rankxplim3  9902  carddom2  10062  wdomnumr  10147  alephordi  10157  alephdom  10164  cardaleph  10172  djuinf  10271  cfsuc  10339  cfsmolem  10352  sornom  10359  fin23lem25  10406  fin1a2lem11  10492  fin1a2s  10496  zorn2lem7  10584  ttukeylem5  10595  alephval2  10661  fpwwe2lem12  10731  gch2  10764  gchaclem  10767  prub  11083  sqgt0sr  11195  1re  11312  lelttr  11404  ltletr  11406  letr  11408  mul0or  11960  prodgt0  12168  mulge0b  12191  squeeze0  12224  sup2  12277  un0addcl  12643  un0mulcl  12644  nn0sub  12660  elnnz  12707  zindd  12804  rpneg  13158  xrlttri  13272  xrlelttr  13289  xrltletr  13290  xrletr  13291  qextlt  13337  qextle  13338  xmullem2  13399  xlemul1a  13422  xrsupexmnf  13439  xrinfmexpnf  13440  supxrun  13450  prunioo  13616  difreicc  13619  iccsplit  13620  uzsplit  13734  fzm1  13745  expcl2lem  14220  expeq0  14239  expnegz  14243  expaddz  14253  expmulz  14255  sqlecan  14357  facdiv  14435  facwordi  14437  bcpasc  14469  resqrex  15423  absexpz  15478  caubnd  15532  summo  15889  zsum  15890  zprod  16110  rpnnen2lem12  16399  ordvdsmul  16476  nn0rppwr  16741  nn0expgcd  16744  dvdsprime  16868  2mulprm  16874  ge2nprmge4  16883  prmdvdsexpr  16899  prmfac1  16902  pythagtriplem2  17001  4sqlem11  17139  vdwlem6  17170  vdwlem9  17173  vdwlem13  17177  cshwshashlem3  17281  prmlem0  17289  pleval2  18515  pltletr  18521  plelttr  18522  tsrlemax  18766  smndex1mgm  19112  f1omvdco2  19668  psgnunilem2  19715  efgredlemc  19965  frgpuptinv  19991  lt6abl  20115  dmdprdsplit2lem  20267  domneq0  20966  lvecvs0or  21392  unichnlidl  21522  baspartn  23278  0top  23307  indistopon  23325  restntr  23506  cnindis  23616  cmpfi  23732  filconn  24208  ufprim  24234  ufildr  24256  alexsubALTlem2  24373  alexsubALTlem3  24374  alexsubALTlem4  24375  ovolicc2lem3  25846  rolle  26316  dvivthlem1  26334  coeaddlem  26574  dgrco  26600  plymul0or  26605  aalioulem3  26667  cxpge0  27017  cxpmul2z  27025  cxpcn3lem  27081  scvxcvx  27319  sqf11  27472  ppiublem1  27535  lgsdir2lem2  27659  lgsqrlem2  27680  2sqnn0  27771  2sqnn  27772  fltoprmgt3  28002  nosepon  28028  nolesgn2ores  28035  nogesgn1ores  28037  nosepne  28043  nolt02o  28058  nosupbnd1lem5  28075  madebdaylemlrcut  28291  madebday  28292  ltslpss  28300  addsproplem2  28362  leadds1  28381  addsuniflem  28393  mulsproplem9  28516  sltmuls1  28539  sltmuls2  28540  muls0ord  28577  precsexlem9  28607  precsexlem11  28609  recsex  28611  abssnid  28635  ltonold  28653  onnolt  28658  eucliddivs  28768  elnnzs  28793  expsne0  28828  bdaypw2n0bndlem  28855  bdayfinbndlem1  28859  z12zsodd  28874  lmieu  29295  upgrpredgv  29723  edglnl  29727  eucrct2eupth  30852  frgrogt3nreg  31004  nvmul0or  31258  hvmul0or  31633  snsssng  33158  disjxpin  33230  expgt0b  33455  axprALT2  35787  j0ltaleph  35948  subfacp1lem4  36035  satfvsucsuc  36217  satfrnmapom  36222  sat1el2xp  36231  gonarlem  36246  gonar  36247  goalrlem  36248  goalr  36249  fmlasucdisj  36251  satffunlem1lem1  36254  satffunlem2lem1  36256  untsucf  36568  dfon2lem6  36643  broutsideof2  36980  btwnoutside  36983  broutsideof3  36984  outsideoftr  36987  lineunray  37005  lineelsb2  37006  nmuladdss  37055  ltnadd  37060  nadddilem4  37065  finminlem  37199  nn0prpw  37204  refssfne  37239  meran1  37292  ontgval  37312  ordcmp  37328  axtcond  37359  bj-sngltag  37989  bj-axseprep  38083  bj-prmoore  38129  topdifinfindis  38363  icoreclin  38374  rdgssun  38395  finxpsuclem  38414  poimirlem24  38656  poimirlem25  38657  poimirlem29  38661  poimirlem31  38663  mblfinlem2  38670  ovoliunnfl  38674  itg2addnclem  38683  sdclem2  38770  fdc  38773  divrngidl  39056  lkreqN  40321  cvrnbtwn4  40430  4atlem12  40763  elpaddn0  40951  paddasslem17  40987  paddidm  40992  pmapjoin  41003  llnexchb2  41020  dalawlem13  41034  dalawlem14  41035  dochkrshp4  42540  lcfl6  42651  lcmineqlem  43196  primrootspoweq0  43250  aks6d1c1  43260  sticksstones22  43312  aks6d1c6lem3  43316  oexpreposd  43473  expeqidd  43476  sn-remul0ord  43553  sn-sup2  43649  fphpdo  43918  pellfundex  43987  jm2.19lem4  44093  jm2.26a  44101  ordnexbtwnsuc  44363  onov0suclim  44370  oege2  44403  succlg  44424  dflim5  44425  oacl2g  44426  omcl2  44429  omcl3g  44430  naddgeoa  44490  safesnsupfiss  44510  fzunt  44550  fzuntd  44551  fzunt1d  44552  fzuntgd  44553  relexpmulg  44804  relexp01min  44807  relexpxpmin  44811  relexpaddss  44812  clsk1indlem3  45137  or2expropbi  48198  ich2exprop  48647  poprelb  48700  reuopreuprim  48702  goldbachthlem2  48725  nprmdvdsfacm1lem2  48800  nprmdvdsfacm1  48803  requad01  48813  evenltle  48909  gbowge7  48955  bgoldbtbndlem3  48999  elclnbgrelnbgr  49017  clnbgrel  49020  dfclnbgr6  49048  dfnbgr6  49049  dfsclnbgr6  49050  upgrimpths  49101  clnbgrgrim  49126  isubgr3stgrlem4  49161  isubgr3stgrlem7  49164  grlimgredgex  49192  gpgedgvtx1  49254  gpgvtxedg0  49255  gpgvtxedg1  49256  lidldomn1  49422  uzlidlring  49426  line2y  49961  itschlc0xyqsol1  49972  itsclc0xyqsolr  49975  inlinecirc02plem  49992