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  888  pm2.621  896  pm2.63  938  jaao  952  jaodan  955  ecase2dOLD  1028  ecase3d  1031  dedlema  1043  dedlemb  1044  cad0  1620  cad0OLD  1621  psssstr  4041  eqoreldif  4621  opthpr  4783  prel12g  4795  opthprneg  4796  sotric  5527  sotr2  5531  relop  5753  suctr  6343  trsucss  6345  ordelinel  6358  fununi  6502  fnprb  7077  soisoi  7192  ordunisuc2  7682  poxp  7957  soxp  7958  frrlem12  8101  frrlem13  8102  wfrlem14OLD  8141  wfrlem15OLD  8142  tfrlem11  8207  omordi  8385  om00  8394  odi  8398  omeulem2  8402  oewordi  8410  nnmordi  8450  omsmolem  8475  swoord2  8518  nneneq  8980  nneneqOLD  8992  dffi3  9178  inf3lem6  9379  cantnfle  9417  cantnflem1  9435  cantnflem2  9436  ttrcltr  9462  r1sdom  9520  r1ord3g  9525  rankxplim3  9627  carddom2  9723  wdomnumr  9808  alephordi  9818  alephdom  9825  cardaleph  9833  djuinf  9932  cfsuc  10001  cfsmolem  10014  sornom  10021  fin23lem25  10068  fin1a2lem11  10154  fin1a2s  10158  zorn2lem7  10246  ttukeylem5  10257  alephval2  10316  fpwwe2lem12  10386  gch2  10419  gchaclem  10422  prub  10738  sqgt0sr  10850  1re  10963  lelttr  11053  ltletr  11055  letr  11057  mul0or  11603  prodgt0  11810  mulge0b  11833  squeeze0  11866  sup2  11919  nnne0  11995  un0addcl  12254  un0mulcl  12255  nn0sub  12271  elnnz  12317  zindd  12409  rpneg  12750  xrlttri  12861  xrlelttr  12878  xrltletr  12879  xrletr  12880  qextlt  12925  qextle  12926  xmullem2  12987  xlemul1a  13010  xrsupexmnf  13027  xrinfmexpnf  13028  supxrun  13038  prunioo  13201  difreicc  13204  iccsplit  13205  uzsplit  13316  fzm1  13324  expcl2lem  13782  expeq0  13801  expnegz  13805  expaddz  13815  expmulz  13817  sqlecan  13913  facdiv  13989  facwordi  13991  bcpasc  14023  resqrex  14950  absexpz  15005  caubnd  15058  summo  15417  zsum  15418  zprod  15635  rpnnen2lem12  15922  ordvdsmul  15997  dvdsprime  16380  2mulprm  16386  ge2nprmge4  16394  prmdvdsexpr  16410  prmfac1  16414  pythagtriplem2  16506  4sqlem11  16644  vdwlem6  16675  vdwlem9  16678  vdwlem13  16682  cshwshashlem3  16787  prmlem0  16795  pleval2  18043  pltletr  18049  plelttr  18050  tsrlemax  18292  smndex1mgm  18534  f1omvdco2  19044  psgnunilem2  19091  efgredlemc  19339  frgpuptinv  19365  lt6abl  19484  dmdprdsplit2lem  19636  drngmul0or  20000  lvecvs0or  20358  domneq0  20556  baspartn  22092  0top  22121  indistopon  22139  restntr  22321  cnindis  22431  cmpfi  22547  filconn  23022  ufprim  23048  ufildr  23070  alexsubALTlem2  23187  alexsubALTlem3  23188  alexsubALTlem4  23189  ovolicc2lem3  24671  rolle  25142  dvivthlem1  25160  coeaddlem  25398  dgrco  25424  plymul0or  25429  aalioulem3  25482  cxpge0  25826  cxpmul2z  25834  cxpcn3lem  25888  scvxcvx  26123  sqf11  26276  ppiublem1  26338  lgsdir2lem2  26462  lgsqrlem2  26483  2sqnn0  26574  2sqnn  26575  lmieu  27133  upgrpredgv  27497  edglnl  27501  eucrct2eupth  28595  frgrogt3nreg  28747  nvmul0or  28998  hvmul0or  29373  snsssng  30846  disjxpin  30913  subfacp1lem4  33131  satfvsucsuc  33313  satfrnmapom  33318  sat1el2xp  33327  gonarlem  33342  gonar  33343  goalrlem  33344  goalr  33345  fmlasucdisj  33347  satffunlem1lem1  33350  satffunlem2lem1  33352  untsucf  33637  sotr3  33719  dfon2lem6  33750  nosepon  33854  nolesgn2ores  33861  nogesgn1ores  33863  nosepne  33869  nolt02o  33884  nosupbnd1lem5  33901  madebdaylemlrcut  34065  madebday  34066  sltlpss  34073  broutsideof2  34410  btwnoutside  34413  broutsideof3  34414  outsideoftr  34417  lineunray  34435  lineelsb2  34436  finminlem  34493  nn0prpw  34498  refssfne  34533  meran1  34586  ontgval  34606  ordcmp  34622  bj-sngltag  35159  bj-prmoore  35272  topdifinfindis  35503  icoreclin  35514  rdgssun  35535  finxpsuclem  35554  poimirlem24  35787  poimirlem25  35788  poimirlem29  35792  poimirlem31  35794  mblfinlem2  35801  ovoliunnfl  35805  itg2addnclem  35814  sdclem2  35886  fdc  35889  divrngidl  36172  lkreqN  37170  cvrnbtwn4  37279  4atlem12  37612  elpaddn0  37800  paddasslem17  37836  paddidm  37841  pmapjoin  37852  llnexchb2  37869  dalawlem13  37883  dalawlem14  37884  dochkrshp4  39389  lcfl6  39500  lcmineqlem  40046  sticksstones22  40110  oexpreposd  40307  nn0rppwr  40319  nn0expgcd  40321  sn-sup2  40425  fphpdo  40625  pellfundex  40694  jm2.19lem4  40800  jm2.26a  40808  relexpmulg  41277  relexp01min  41280  relexpxpmin  41284  relexpaddss  41285  clsk1indlem3  41612  or2expropbi  44484  ich2exprop  44879  poprelb  44932  reuopreuprim  44934  goldbachthlem2  44954  requad01  45029  evenltle  45125  gbowge7  45171  bgoldbtbndlem3  45215  lidldomn1  45435  uzlidlring  45443  prelrrx2b  46016  line2y  46057  itschlc0xyqsol1  46068  itsclc0xyqsolr  46071  inlinecirc02plem  46088