Theorem jaod 856

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 32	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 32	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 854	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  mpjaod  857  orel2  887  pm2.621  895  pm2.63  937  jaao  951  jaodan  954  ecase2dOLD  1027  ecase3d  1030  dedlema  1042  dedlemb  1043  cad0  1611  cad0OLD  1612  psssstr  4101  eqoreldif  4683  opthpr  4847  prel12g  4859  opthprneg  4860  sotric  5609  sotr2  5613  sotr3  5620  relop  5844  suctr  6444  trsucss  6446  ordelinel  6459  fununi  6617  fnprb  7205  soisoi  7321  ordunisuc2  7830  poxp  8114  soxp  8115  frrlem12  8283  frrlem13  8284  wfrlem14OLD  8323  wfrlem15OLD  8324  tfrlem11  8389  omordi  8567  om00  8576  odi  8580  omeulem2  8584  oewordi  8592  nnmordi  8632  omsmolem  8658  swoord2  8737  nneneq  9211  nneneqOLD  9223  dffi3  9428  inf3lem6  9630  cantnfle  9668  cantnflem1  9686  cantnflem2  9687  ttrcltr  9713  r1sdom  9771  r1ord3g  9776  rankxplim3  9878  carddom2  9974  wdomnumr  10061  alephordi  10071  alephdom  10078  cardaleph  10086  djuinf  10185  cfsuc  10254  cfsmolem  10267  sornom  10274  fin23lem25  10321  fin1a2lem11  10407  fin1a2s  10411  zorn2lem7  10499  ttukeylem5  10510  alephval2  10569  fpwwe2lem12  10639  gch2  10672  gchaclem  10675  prub  10991  sqgt0sr  11103  1re  11218  lelttr  11308  ltletr  11310  letr  11312  mul0or  11858  prodgt0  12065  mulge0b  12088  squeeze0  12121  sup2  12174  un0addcl  12509  un0mulcl  12510  nn0sub  12526  elnnz  12572  zindd  12667  rpneg  13012  xrlttri  13124  xrlelttr  13141  xrltletr  13142  xrletr  13143  qextlt  13188  qextle  13189  xmullem2  13250  xlemul1a  13273  xrsupexmnf  13290  xrinfmexpnf  13291  supxrun  13301  prunioo  13464  difreicc  13467  iccsplit  13468  uzsplit  13579  fzm1  13587  expcl2lem  14044  expeq0  14063  expnegz  14067  expaddz  14077  expmulz  14079  sqlecan  14178  facdiv  14252  facwordi  14254  bcpasc  14286  resqrex  15203  absexpz  15258  caubnd  15311  summo  15669  zsum  15670  zprod  15887  rpnnen2lem12  16175  ordvdsmul  16250  dvdsprime  16631  2mulprm  16637  ge2nprmge4  16645  prmdvdsexpr  16661  prmfac1  16665  pythagtriplem2  16759  4sqlem11  16897  vdwlem6  16928  vdwlem9  16931  vdwlem13  16935  cshwshashlem3  17040  prmlem0  17048  pleval2  18302  pltletr  18308  plelttr  18309  tsrlemax  18551  smndex1mgm  18832  f1omvdco2  19368  psgnunilem2  19415  efgredlemc  19665  frgpuptinv  19691  lt6abl  19815  dmdprdsplit2lem  19967  drngmul0or  20616  lvecvs0or  20959  domneq0  21207  baspartn  22812  0top  22841  indistopon  22859  restntr  23041  cnindis  23151  cmpfi  23267  filconn  23742  ufprim  23768  ufildr  23790  alexsubALTlem2  23907  alexsubALTlem3  23908  alexsubALTlem4  23909  ovolicc2lem3  25403  rolle  25877  dvivthlem1  25896  coeaddlem  26138  dgrco  26165  plymul0or  26170  aalioulem3  26224  cxpge0  26572  cxpmul2z  26580  cxpcn3lem  26637  scvxcvx  26873  sqf11  27026  ppiublem1  27090  lgsdir2lem2  27214  lgsqrlem2  27235  2sqnn0  27326  2sqnn  27327  nosepon  27553  nolesgn2ores  27560  nogesgn1ores  27562  nosepne  27568  nolt02o  27583  nosupbnd1lem5  27600  madebdaylemlrcut  27780  madebday  27781  sltlpss  27788  addsproplem2  27842  sleadd1  27861  addsuniflem  27873  mulsproplem9  27979  ssltmul1  28002  ssltmul2  28003  muls0ord  28040  precsexlem9  28068  precsexlem11  28070  recsex  28072  abssnid  28092  sltonold  28108  lmieu  28543  upgrpredgv  28907  edglnl  28911  eucrct2eupth  30007  frgrogt3nreg  30159  nvmul0or  30412  hvmul0or  30787  snsssng  32261  disjxpin  32328  subfacp1lem4  34702  satfvsucsuc  34884  satfrnmapom  34889  sat1el2xp  34898  gonarlem  34913  gonar  34914  goalrlem  34915  goalr  34916  fmlasucdisj  34918  satffunlem1lem1  34921  satffunlem2lem1  34923  untsucf  35213  dfon2lem6  35293  broutsideof2  35627  btwnoutside  35630  broutsideof3  35631  outsideoftr  35634  lineunray  35652  lineelsb2  35653  finminlem  35711  nn0prpw  35716  refssfne  35751  meran1  35804  ontgval  35824  ordcmp  35840  bj-sngltag  36371  bj-prmoore  36503  topdifinfindis  36734  icoreclin  36745  rdgssun  36766  finxpsuclem  36785  poimirlem24  37025  poimirlem25  37026  poimirlem29  37030  poimirlem31  37032  mblfinlem2  37039  ovoliunnfl  37043  itg2addnclem  37052  sdclem2  37123  fdc  37126  divrngidl  37409  lkreqN  38553  cvrnbtwn4  38662  4atlem12  38996  elpaddn0  39184  paddasslem17  39220  paddidm  39225  pmapjoin  39236  llnexchb2  39253  dalawlem13  39267  dalawlem14  39268  dochkrshp4  40773  lcfl6  40884  lcmineqlem  41434  aks6d1c1  41494  sticksstones22  41546  aks6d1c6lem3  41550  oexpreposd  41782  nn0rppwr  41794  nn0expgcd  41796  sn-sup2  41925  fphpdo  42138  pellfundex  42207  jm2.19lem4  42314  jm2.26a  42322  ordnexbtwnsuc  42598  onov0suclim  42605  oege2  42638  succlg  42659  dflim5  42660  oacl2g  42661  omcl2  42664  omcl3g  42665  naddgeoa  42726  safesnsupfiss  42747  fzunt  42787  fzuntd  42788  fzunt1d  42789  fzuntgd  42790  relexpmulg  43042  relexp01min  43045  relexpxpmin  43049  relexpaddss  43050  clsk1indlem3  43375  or2expropbi  46321  ich2exprop  46716  poprelb  46769  reuopreuprim  46771  goldbachthlem2  46791  requad01  46866  evenltle  46962  gbowge7  47008  bgoldbtbndlem3  47052  lidldomn1  47186  uzlidlring  47190  prelrrx2b  47680  line2y  47721  itschlc0xyqsol1  47732  itsclc0xyqsolr  47735  inlinecirc02plem  47752