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  4040  eqoreldif  4647  opthpr  4811  prel12g  4824  opthprneg  4825  axpr  5396  sotric  5596  sotr2  5600  sotr3  5607  relop  5838  suctr  6477  trsucss  6479  ordelinel  6492  fununi  6645  fnprb  7245  soisoi  7367  ordunisuc2  7889  poxp  8177  soxp  8178  frrlem12  8353  frrlem13  8354  tfrlem11  8434  onelfvnef1  8487  omordi  8612  om00  8621  odi  8625  omeulem2  8629  oewordi  8638  nnmordi  8678  omsmolem  8704  swoord2  8789  nneneq  9259  dffi3  9460  inf3lem6  9671  cantnfle  9709  cantnflem1  9727  cantnflem2  9728  ttrcltr  9754  r1sdom  9818  r1ord3g  9823  rankxplim3  9935  carddom2  10095  wdomnumr  10182  alephordi  10192  alephdom  10199  cardaleph  10207  djuinf  10306  cfsuc  10374  cfsmolem  10387  sornom  10394  fin23lem25  10441  fin1a2lem11  10527  fin1a2s  10531  zorn2lem7  10619  ttukeylem5  10630  alephval2  10696  fpwwe2lem12  10766  gch2  10799  gchaclem  10802  prub  11118  sqgt0sr  11230  1re  11347  lelttr  11439  ltletr  11441  letr  11443  mul0or  11996  prodgt0  12204  mulge0b  12227  squeeze0  12260  sup2  12313  un0addcl  12679  un0mulcl  12680  nn0sub  12696  elnnz  12743  zindd  12840  rpneg  13194  xrlttri  13308  xrlelttr  13325  xrltletr  13326  xrletr  13327  qextlt  13373  qextle  13374  xmullem2  13435  xlemul1a  13458  xrsupexmnf  13475  xrinfmexpnf  13476  supxrun  13486  prunioo  13652  difreicc  13655  iccsplit  13656  uzsplit  13770  fzm1  13781  expcl2lem  14256  expeq0  14275  expnegz  14279  expaddz  14289  expmulz  14291  sqlecan  14393  facdiv  14472  facwordi  14474  bcpasc  14506  resqrex  15460  absexpz  15515  caubnd  15570  summo  15927  zsum  15928  zprod  16148  rpnnen2lem12  16437  ordvdsmul  16514  nn0rppwr  16779  nn0expgcd  16782  dvdsprime  16906  2mulprm  16912  ge2nprmge4  16921  prmdvdsexpr  16937  prmfac1  16940  pythagtriplem2  17039  4sqlem11  17177  vdwlem6  17208  vdwlem9  17211  vdwlem13  17215  cshwshashlem3  17319  prmlem0  17327  pleval2  18559  pltletr  18565  plelttr  18566  tsrlemax  18810  smndex1mgm  19156  f1omvdco2  19713  psgnunilem2  19760  efgredlemc  20010  frgpuptinv  20036  lt6abl  20160  dmdprdsplit2lem  20312  domneq0  21011  lvecvs0or  21437  unichnlidl  21567  baspartn  23327  0top  23356  indistopon  23374  restntr  23555  cnindis  23665  cmpfi  23781  filconn  24257  ufprim  24283  ufildr  24305  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALTlem4  24424  ovolicc2lem3  25895  rolle  26365  dvivthlem1  26383  coeaddlem  26623  dgrco  26649  plymul0or  26654  aalioulem3  26718  cxpge0  27068  cxpmul2z  27076  cxpcn3lem  27132  scvxcvx  27370  sqf11  27523  ppiublem1  27586  lgsdir2lem2  27710  lgsqrlem2  27731  2sqnn0  27822  2sqnn  27823  fltoprmgt3  28053  nosepon  28079  nolesgn2ores  28086  nogesgn1ores  28088  nosepne  28094  nolt02o  28109  nosupbnd1lem5  28126  madebdaylemlrcut  28342  madebday  28343  ltslpss  28351  addsproplem2  28413  leadds1  28432  addsuniflem  28444  mulsproplem9  28567  sltmuls1  28590  sltmuls2  28591  muls0ord  28628  precsexlem9  28658  precsexlem11  28660  recsex  28662  abssnid  28686  ltonold  28704  onnolt  28709  eucliddivs  28819  elnnzs  28844  expsne0  28879  bdaypw2n0bndlem  28906  bdayfinbndlem1  28910  z12zsodd  28925  lmieu  29346  upgrpredgv  29774  edglnl  29778  eucrct2eupth  30903  frgrogt3nreg  31055  nvmul0or  31309  hvmul0or  31684  snsssng  33209  disjxpin  33280  expgt0b  33504  axprALT2  35857  j0ltaleph  36049  subfacp1lem4  36156  satfvsucsuc  36338  satfrnmapom  36343  sat1el2xp  36352  gonarlem  36367  gonar  36368  goalrlem  36369  goalr  36370  fmlasucdisj  36372  satffunlem1lem1  36375  satffunlem2lem1  36377  untsucf  36690  dfon2lem6  36765  broutsideof2  37102  btwnoutside  37105  broutsideof3  37106  outsideoftr  37109  lineunray  37127  lineelsb2  37128  nmuladdss  37177  ltnadd  37182  nadddilem4  37187  finminlem  37321  nn0prpw  37326  refssfne  37361  meran1  37414  ontgval  37434  ordcmp  37450  axtcond  37481  bj-sngltag  38111  bj-axseprep  38260  bj-prmoore  38306  topdifinfindis  38537  icoreclin  38548  rdgssun  38569  finxpsuclem  38588  poimirlem24  38830  poimirlem25  38831  poimirlem29  38835  poimirlem31  38837  mblfinlem2  38844  ovoliunnfl  38848  itg2addnclem  38857  sdclem2  38942  fdc  38945  divrngidl  39228  lkreqN  40493  cvrnbtwn4  40602  4atlem12  40935  elpaddn0  41123  paddasslem17  41159  paddidm  41164  pmapjoin  41175  llnexchb2  41192  dalawlem13  41206  dalawlem14  41207  dochkrshp4  42712  lcfl6  42823  lcmineqlem  43368  primrootspoweq0  43422  aks6d1c1  43432  sticksstones22  43484  aks6d1c6lem3  43488  oexpreposd  43645  expeqidd  43648  sn-remul0ord  43725  sn-sup2  43821  fphpdo  44090  pellfundex  44159  jm2.19lem4  44265  jm2.26a  44273  ordnexbtwnsuc  44530  onov0suclim  44537  oege2  44570  succlg  44591  dflim5  44592  oacl2g  44593  omcl2  44596  omcl3g  44597  naddgeoa  44657  safesnsupfiss  44677  fzunt  44717  fzuntd  44718  fzunt1d  44719  fzuntgd  44720  relexpmulg  44971  relexp01min  44974  relexpxpmin  44978  relexpaddss  44979  clsk1indlem3  45304  or2expropbi  48377  ich2exprop  48826  poprelb  48879  reuopreuprim  48881  goldbachthlem2  48904  nprmdvdsfacm1lem2  48979  nprmdvdsfacm1  48982  requad01  48992  evenltle  49088  gbowge7  49134  bgoldbtbndlem3  49178  elclnbgrelnbgr  49196  clnbgrel  49199  dfclnbgr6  49227  dfnbgr6  49228  dfsclnbgr6  49229  upgrimpths  49280  clnbgrgrim  49305  isubgr3stgrlem4  49340  isubgr3stgrlem7  49343  grlimgredgex  49371  gpgedgvtx1  49433  gpgvtxedg0  49434  gpgvtxedg1  49435  lidldomn1  49601  uzlidlring  49605  line2y  50198  itschlc0xyqsol1  50209  itsclc0xyqsolr  50212  inlinecirc02plem  50229