Theorem jaod 858

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  mpjaod  859  orel2  890  pm2.621  898  pm2.63  940  jaao  954  jaodan  957  ecase2dOLD  1030  ecase3d  1033  dedlema  1045  dedlemb  1046  cad0  1620  cad0OLD  1621  psssstr  4106  eqoreldif  4688  opthpr  4852  prel12g  4864  opthprneg  4865  sotric  5616  sotr2  5620  sotr3  5627  relop  5849  suctr  6448  trsucss  6450  ordelinel  6463  fununi  6621  fnprb  7207  soisoi  7322  ordunisuc2  7830  poxp  8111  soxp  8112  frrlem12  8279  frrlem13  8280  wfrlem14OLD  8319  wfrlem15OLD  8320  tfrlem11  8385  omordi  8563  om00  8572  odi  8576  omeulem2  8580  oewordi  8588  nnmordi  8628  omsmolem  8653  swoord2  8732  nneneq  9206  nneneqOLD  9218  dffi3  9423  inf3lem6  9625  cantnfle  9663  cantnflem1  9681  cantnflem2  9682  ttrcltr  9708  r1sdom  9766  r1ord3g  9771  rankxplim3  9873  carddom2  9969  wdomnumr  10056  alephordi  10066  alephdom  10073  cardaleph  10081  djuinf  10180  cfsuc  10249  cfsmolem  10262  sornom  10269  fin23lem25  10316  fin1a2lem11  10402  fin1a2s  10406  zorn2lem7  10494  ttukeylem5  10505  alephval2  10564  fpwwe2lem12  10634  gch2  10667  gchaclem  10670  prub  10986  sqgt0sr  11098  1re  11211  lelttr  11301  ltletr  11303  letr  11305  mul0or  11851  prodgt0  12058  mulge0b  12081  squeeze0  12114  sup2  12167  un0addcl  12502  un0mulcl  12503  nn0sub  12519  elnnz  12565  zindd  12660  rpneg  13003  xrlttri  13115  xrlelttr  13132  xrltletr  13133  xrletr  13134  qextlt  13179  qextle  13180  xmullem2  13241  xlemul1a  13264  xrsupexmnf  13281  xrinfmexpnf  13282  supxrun  13292  prunioo  13455  difreicc  13458  iccsplit  13459  uzsplit  13570  fzm1  13578  expcl2lem  14036  expeq0  14055  expnegz  14059  expaddz  14069  expmulz  14071  sqlecan  14170  facdiv  14244  facwordi  14246  bcpasc  14278  resqrex  15194  absexpz  15249  caubnd  15302  summo  15660  zsum  15661  zprod  15878  rpnnen2lem12  16165  ordvdsmul  16240  dvdsprime  16621  2mulprm  16627  ge2nprmge4  16635  prmdvdsexpr  16651  prmfac1  16655  pythagtriplem2  16747  4sqlem11  16885  vdwlem6  16916  vdwlem9  16919  vdwlem13  16923  cshwshashlem3  17028  prmlem0  17036  pleval2  18287  pltletr  18293  plelttr  18294  tsrlemax  18536  smndex1mgm  18785  f1omvdco2  19311  psgnunilem2  19358  efgredlemc  19608  frgpuptinv  19634  lt6abl  19758  dmdprdsplit2lem  19910  drngmul0or  20337  lvecvs0or  20714  domneq0  20906  baspartn  22449  0top  22478  indistopon  22496  restntr  22678  cnindis  22788  cmpfi  22904  filconn  23379  ufprim  23405  ufildr  23427  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALTlem4  23546  ovolicc2lem3  25028  rolle  25499  dvivthlem1  25517  coeaddlem  25755  dgrco  25781  plymul0or  25786  aalioulem3  25839  cxpge0  26183  cxpmul2z  26191  cxpcn3lem  26245  scvxcvx  26480  sqf11  26633  ppiublem1  26695  lgsdir2lem2  26819  lgsqrlem2  26840  2sqnn0  26931  2sqnn  26932  nosepon  27158  nolesgn2ores  27165  nogesgn1ores  27167  nosepne  27173  nolt02o  27188  nosupbnd1lem5  27205  madebdaylemlrcut  27383  madebday  27384  sltlpss  27391  addsproplem2  27444  sleadd1  27462  addsuniflem  27474  mulsproplem9  27570  ssltmul1  27592  ssltmul2  27593  precsexlem9  27651  precsexlem11  27653  recsex  27655  lmieu  28025  upgrpredgv  28389  edglnl  28393  eucrct2eupth  29488  frgrogt3nreg  29640  nvmul0or  29891  hvmul0or  30266  snsssng  31740  disjxpin  31807  subfacp1lem4  34163  satfvsucsuc  34345  satfrnmapom  34350  sat1el2xp  34359  gonarlem  34374  gonar  34375  goalrlem  34376  goalr  34377  fmlasucdisj  34379  satffunlem1lem1  34382  satffunlem2lem1  34384  untsucf  34668  dfon2lem6  34749  broutsideof2  35083  btwnoutside  35086  broutsideof3  35087  outsideoftr  35090  lineunray  35108  lineelsb2  35109  finminlem  35192  nn0prpw  35197  refssfne  35232  meran1  35285  ontgval  35305  ordcmp  35321  bj-sngltag  35853  bj-prmoore  35985  topdifinfindis  36216  icoreclin  36227  rdgssun  36248  finxpsuclem  36267  poimirlem24  36501  poimirlem25  36502  poimirlem29  36506  poimirlem31  36508  mblfinlem2  36515  ovoliunnfl  36519  itg2addnclem  36528  sdclem2  36599  fdc  36602  divrngidl  36885  lkreqN  38029  cvrnbtwn4  38138  4atlem12  38472  elpaddn0  38660  paddasslem17  38696  paddidm  38701  pmapjoin  38712  llnexchb2  38729  dalawlem13  38743  dalawlem14  38744  dochkrshp4  40249  lcfl6  40360  lcmineqlem  40906  sticksstones22  40973  oexpreposd  41208  nn0rppwr  41220  nn0expgcd  41222  sn-sup2  41339  fphpdo  41541  pellfundex  41610  jm2.19lem4  41717  jm2.26a  41725  ordnexbtwnsuc  42003  onov0suclim  42010  oege2  42043  succlg  42064  dflim5  42065  oacl2g  42066  omcl2  42069  omcl3g  42070  naddgeoa  42131  safesnsupfiss  42152  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  relexpmulg  42447  relexp01min  42450  relexpxpmin  42454  relexpaddss  42455  clsk1indlem3  42780  or2expropbi  45731  ich2exprop  46126  poprelb  46179  reuopreuprim  46181  goldbachthlem2  46201  requad01  46276  evenltle  46372  gbowge7  46418  bgoldbtbndlem3  46462  lidldomn1  46777  uzlidlring  46781  prelrrx2b  47354  line2y  47395  itschlc0xyqsol1  47406  itsclc0xyqsolr  47409  inlinecirc02plem  47426