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 209  df-or 844

This theorem is referenced by:  mpjaod  856  orel2  887  pm2.621  895  pm2.63  937  jaao  951  jaodan  954  ecase2d  1026  ecase3d  1029  dedlema  1040  dedlemb  1041  cad0  1617  psssstr  4086  eqoreldif  4625  opthpr  4785  prel12g  4797  opthprneg  4798  sotric  5504  sotr2  5508  relop  5724  suctr  6277  trsucss  6279  ordelinel  6292  fununi  6432  fnprb  6974  soisoi  7084  ordunisuc2  7562  poxp  7825  soxp  7826  wfrlem14  7971  wfrlem15  7972  tfrlem11  8027  omordi  8195  om00  8204  odi  8208  omeulem2  8212  oewordi  8220  nnmordi  8260  omsmolem  8283  swoord2  8324  nneneq  8703  dffi3  8898  inf3lem6  9099  cantnfle  9137  cantnflem1  9155  cantnflem2  9156  r1sdom  9206  r1ord3g  9211  rankxplim3  9313  carddom2  9409  wdomnumr  9493  alephordi  9503  alephdom  9510  cardaleph  9518  djuinf  9617  cfsuc  9682  cfsmolem  9695  sornom  9702  fin23lem25  9749  fin1a2lem11  9835  fin1a2s  9839  zorn2lem7  9927  ttukeylem5  9938  alephval2  9997  fpwwe2lem13  10067  gch2  10100  gchaclem  10103  prub  10419  sqgt0sr  10531  1re  10644  lelttr  10734  ltletr  10735  letr  10737  mul0or  11283  prodgt0  11490  mulge0b  11513  squeeze0  11546  sup2  11600  nnne0  11674  un0addcl  11933  un0mulcl  11934  nn0sub  11950  elnnz  11994  zindd  12086  rpneg  12424  xrlttri  12535  xrlelttr  12552  xrltletr  12553  xrletr  12554  qextlt  12599  qextle  12600  xmullem2  12661  xlemul1a  12684  xrsupexmnf  12701  xrinfmexpnf  12702  supxrun  12712  prunioo  12870  difreicc  12873  iccsplit  12874  uzsplit  12982  fzm1  12990  expcl2lem  13444  expeq0  13462  expnegz  13466  expaddz  13476  expmulz  13478  sqlecan  13574  facdiv  13650  facwordi  13652  bcpasc  13684  resqrex  14613  absexpz  14668  caubnd  14721  summo  15077  zsum  15078  zprod  15294  rpnnen2lem12  15581  ordvdsmul  15653  dvdsprime  16034  2mulprm  16040  ge2nprmge4  16048  prmdvdsexpr  16064  prmfac1  16066  pythagtriplem2  16157  4sqlem11  16294  vdwlem6  16325  vdwlem9  16328  vdwlem13  16332  cshwshashlem3  16434  prmlem0  16442  pleval2  17578  pltletr  17584  plelttr  17585  tsrlemax  17833  smndex1mgm  18075  f1omvdco2  18579  psgnunilem2  18626  efgredlemc  18874  frgpuptinv  18900  lt6abl  19018  dmdprdsplit2lem  19170  drngmul0or  19526  lvecvs0or  19883  domneq0  20073  baspartn  21565  0top  21594  indistopon  21612  restntr  21793  cnindis  21903  cmpfi  22019  filconn  22494  ufprim  22520  ufildr  22542  alexsubALTlem2  22659  alexsubALTlem3  22660  alexsubALTlem4  22661  ovolicc2lem3  24123  rolle  24590  dvivthlem1  24608  coeaddlem  24842  dgrco  24868  plymul0or  24873  aalioulem3  24926  cxpge0  25269  cxpmul2z  25277  cxpcn3lem  25331  scvxcvx  25566  sqf11  25719  ppiublem1  25781  lgsdir2lem2  25905  lgsqrlem2  25926  2sqnn0  26017  2sqnn  26018  lmieu  26573  upgrpredgv  26927  edglnl  26931  eucrct2eupth  28027  frgrogt3nreg  28179  nvmul0or  28430  hvmul0or  28805  disjxpin  30341  subfacp1lem4  32434  satfvsucsuc  32616  satfrnmapom  32621  sat1el2xp  32630  gonarlem  32645  gonar  32646  goalrlem  32647  goalr  32648  fmlasucdisj  32650  satffunlem1lem1  32653  satffunlem2lem1  32655  untsucf  32940  sotr3  33006  dfon2lem6  33037  dftrpred3g  33076  frrlem12  33138  frrlem13  33139  nosepon  33176  nolesgn2ores  33183  nosepne  33189  nolt02o  33203  nosupbnd1lem5  33216  broutsideof2  33587  btwnoutside  33590  broutsideof3  33591  outsideoftr  33594  lineunray  33612  lineelsb2  33613  finminlem  33670  nn0prpw  33675  refssfne  33710  meran1  33763  ontgval  33783  ordcmp  33799  bj-sngltag  34299  bj-prmoore  34411  topdifinfindis  34631  icoreclin  34642  rdgssun  34663  finxpsuclem  34682  poimirlem24  34920  poimirlem25  34921  poimirlem29  34925  poimirlem31  34927  mblfinlem2  34934  ovoliunnfl  34938  itg2addnclem  34947  sdclem2  35021  fdc  35024  divrngidl  35310  lkreqN  36310  cvrnbtwn4  36419  4atlem12  36752  elpaddn0  36940  paddasslem17  36976  paddidm  36981  pmapjoin  36992  llnexchb2  37009  dalawlem13  37023  dalawlem14  37024  dochkrshp4  38529  lcfl6  38640  oexpreposd  39185  nn0rppwr  39188  nn0expgcd  39190  fphpdo  39420  pellfundex  39489  jm2.19lem4  39595  jm2.26a  39603  relexpmulg  40061  relexp01min  40064  relexpxpmin  40068  relexpaddss  40069  clsk1indlem3  40399  or2expropbi  43276  ich2exprop  43640  poprelb  43693  reuopreuprim  43695  goldbachthlem2  43715  requad01  43793  evenltle  43889  gbowge7  43935  bgoldbtbndlem3  43979  lidldomn1  44199  uzlidlring  44207  prelrrx2b  44708  line2y  44749  itschlc0xyqsol1  44760  itsclc0xyqsolr  44763  inlinecirc02plem  44780