Theorem jaod 855

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 853	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  mpjaod  856  orel2  887  pm2.621  895  pm2.63  937  jaao  951  jaodan  954  ecase2dOLD  1027  ecase3d  1030  dedlema  1042  dedlemb  1043  cad0  1621  cad0OLD  1622  psssstr  4037  eqoreldif  4617  opthpr  4779  prel12g  4791  opthprneg  4792  sotric  5522  sotr2  5526  relop  5748  suctr  6334  trsucss  6336  ordelinel  6349  fununi  6493  fnprb  7066  soisoi  7179  ordunisuc2  7666  poxp  7940  soxp  7941  frrlem12  8084  frrlem13  8085  wfrlem14OLD  8124  wfrlem15OLD  8125  tfrlem11  8190  omordi  8359  om00  8368  odi  8372  omeulem2  8376  oewordi  8384  nnmordi  8424  omsmolem  8447  swoord2  8488  nneneq  8896  dffi3  9120  inf3lem6  9321  cantnfle  9359  cantnflem1  9377  cantnflem2  9378  dftrpred3g  9412  r1sdom  9463  r1ord3g  9468  rankxplim3  9570  carddom2  9666  wdomnumr  9751  alephordi  9761  alephdom  9768  cardaleph  9776  djuinf  9875  cfsuc  9944  cfsmolem  9957  sornom  9964  fin23lem25  10011  fin1a2lem11  10097  fin1a2s  10101  zorn2lem7  10189  ttukeylem5  10200  alephval2  10259  fpwwe2lem12  10329  gch2  10362  gchaclem  10365  prub  10681  sqgt0sr  10793  1re  10906  lelttr  10996  ltletr  10997  letr  10999  mul0or  11545  prodgt0  11752  mulge0b  11775  squeeze0  11808  sup2  11861  nnne0  11937  un0addcl  12196  un0mulcl  12197  nn0sub  12213  elnnz  12259  zindd  12351  rpneg  12691  xrlttri  12802  xrlelttr  12819  xrltletr  12820  xrletr  12821  qextlt  12866  qextle  12867  xmullem2  12928  xlemul1a  12951  xrsupexmnf  12968  xrinfmexpnf  12969  supxrun  12979  prunioo  13142  difreicc  13145  iccsplit  13146  uzsplit  13257  fzm1  13265  expcl2lem  13722  expeq0  13741  expnegz  13745  expaddz  13755  expmulz  13757  sqlecan  13853  facdiv  13929  facwordi  13931  bcpasc  13963  resqrex  14890  absexpz  14945  caubnd  14998  summo  15357  zsum  15358  zprod  15575  rpnnen2lem12  15862  ordvdsmul  15937  dvdsprime  16320  2mulprm  16326  ge2nprmge4  16334  prmdvdsexpr  16350  prmfac1  16354  pythagtriplem2  16446  4sqlem11  16584  vdwlem6  16615  vdwlem9  16618  vdwlem13  16622  cshwshashlem3  16727  prmlem0  16735  pleval2  17970  pltletr  17976  plelttr  17977  tsrlemax  18219  smndex1mgm  18461  f1omvdco2  18971  psgnunilem2  19018  efgredlemc  19266  frgpuptinv  19292  lt6abl  19411  dmdprdsplit2lem  19563  drngmul0or  19927  lvecvs0or  20285  domneq0  20481  baspartn  22012  0top  22041  indistopon  22059  restntr  22241  cnindis  22351  cmpfi  22467  filconn  22942  ufprim  22968  ufildr  22990  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  ovolicc2lem3  24588  rolle  25059  dvivthlem1  25077  coeaddlem  25315  dgrco  25341  plymul0or  25346  aalioulem3  25399  cxpge0  25743  cxpmul2z  25751  cxpcn3lem  25805  scvxcvx  26040  sqf11  26193  ppiublem1  26255  lgsdir2lem2  26379  lgsqrlem2  26400  2sqnn0  26491  2sqnn  26492  lmieu  27049  upgrpredgv  27412  edglnl  27416  eucrct2eupth  28510  frgrogt3nreg  28662  nvmul0or  28913  hvmul0or  29288  snsssng  30761  disjxpin  30828  subfacp1lem4  33045  satfvsucsuc  33227  satfrnmapom  33232  sat1el2xp  33241  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem2lem1  33266  untsucf  33551  sotr3  33639  dfon2lem6  33670  ttrcltr  33702  nosepon  33795  nolesgn2ores  33802  nogesgn1ores  33804  nosepne  33810  nolt02o  33825  nosupbnd1lem5  33842  madebdaylemlrcut  34006  madebday  34007  sltlpss  34014  broutsideof2  34351  btwnoutside  34354  broutsideof3  34355  outsideoftr  34358  lineunray  34376  lineelsb2  34377  finminlem  34434  nn0prpw  34439  refssfne  34474  meran1  34527  ontgval  34547  ordcmp  34563  bj-sngltag  35100  bj-prmoore  35213  topdifinfindis  35444  icoreclin  35455  rdgssun  35476  finxpsuclem  35495  poimirlem24  35728  poimirlem25  35729  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  ovoliunnfl  35746  itg2addnclem  35755  sdclem2  35827  fdc  35830  divrngidl  36113  lkreqN  37111  cvrnbtwn4  37220  4atlem12  37553  elpaddn0  37741  paddasslem17  37777  paddidm  37782  pmapjoin  37793  llnexchb2  37810  dalawlem13  37824  dalawlem14  37825  dochkrshp4  39330  lcfl6  39441  lcmineqlem  39988  sticksstones22  40052  oexpreposd  40242  nn0rppwr  40254  nn0expgcd  40256  sn-sup2  40360  fphpdo  40555  pellfundex  40624  jm2.19lem4  40730  jm2.26a  40738  relexpmulg  41207  relexp01min  41210  relexpxpmin  41214  relexpaddss  41215  clsk1indlem3  41542  or2expropbi  44415  ich2exprop  44811  poprelb  44864  reuopreuprim  44866  goldbachthlem2  44886  requad01  44961  evenltle  45057  gbowge7  45103  bgoldbtbndlem3  45147  lidldomn1  45367  uzlidlring  45375  prelrrx2b  45948  line2y  45989  itschlc0xyqsol1  46000  itsclc0xyqsolr  46003  inlinecirc02plem  46020