Theorem jaod 872

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  mpjaod  873  orel2  903  pm2.621  911  pm2.63  955  jaao  969  jaodan  972  ecase3d  1048  dedlema  1059  dedlemb  1060  cad0  1641  psssstr  4066  eqoreldif  4647  opthpr  4811  prel12g  4824  opthprneg  4825  axpr  5388  sotric  5589  sotr2  5593  sotr3  5600  relop  5826  suctr  6438  trsucss  6440  ordelinel  6453  fununi  6600  fnprb  7196  soisoi  7316  ordunisuc2  7828  poxp  8112  soxp  8113  frrlem12  8282  frrlem13  8283  tfrlem11  8363  omordi  8539  om00  8548  odi  8552  omeulem2  8556  oewordi  8565  nnmordi  8605  omsmolem  8631  swoord2  8716  nneneq  9178  dffi3  9379  inf3lem6  9590  cantnfle  9628  cantnflem1  9646  cantnflem2  9647  ttrcltr  9673  r1sdom  9734  r1ord3g  9739  rankxplim3  9841  carddom2  9951  wdomnumr  10036  alephordi  10046  alephdom  10053  cardaleph  10061  djuinf  10160  cfsuc  10229  cfsmolem  10242  sornom  10249  fin23lem25  10296  fin1a2lem11  10382  fin1a2s  10386  zorn2lem7  10474  ttukeylem5  10485  alephval2  10545  fpwwe2lem12  10615  gch2  10648  gchaclem  10651  prub  10967  sqgt0sr  11079  1re  11196  lelttr  11288  ltletr  11290  letr  11292  mul0or  11842  prodgt0  12050  mulge0b  12073  squeeze0  12106  sup2  12159  un0addcl  12525  un0mulcl  12526  nn0sub  12542  elnnz  12589  zindd  12685  rpneg  13038  xrlttri  13152  xrlelttr  13169  xrltletr  13170  xrletr  13171  qextlt  13217  qextle  13218  xmullem2  13279  xlemul1a  13302  xrsupexmnf  13319  xrinfmexpnf  13320  supxrun  13330  prunioo  13496  difreicc  13499  iccsplit  13500  uzsplit  13612  fzm1  13623  expcl2lem  14097  expeq0  14116  expnegz  14120  expaddz  14130  expmulz  14132  sqlecan  14233  facdiv  14311  facwordi  14313  bcpasc  14345  resqrex  15289  absexpz  15344  caubnd  15398  summo  15756  zsum  15757  zprod  15979  rpnnen2lem12  16269  ordvdsmul  16346  nn0rppwr  16607  nn0expgcd  16610  dvdsprime  16733  2mulprm  16739  ge2nprmge4  16748  prmdvdsexpr  16764  prmfac1  16767  pythagtriplem2  16865  4sqlem11  17003  vdwlem6  17034  vdwlem9  17037  vdwlem13  17041  cshwshashlem3  17145  prmlem0  17153  pleval2  18379  pltletr  18385  plelttr  18386  tsrlemax  18630  smndex1mgm  18957  f1omvdco2  19506  psgnunilem2  19553  efgredlemc  19803  frgpuptinv  19829  lt6abl  19953  dmdprdsplit2lem  20105  domneq0  20781  lvecvs0or  21198  unichnlidl  21328  baspartn  23068  0top  23097  indistopon  23115  restntr  23296  cnindis  23406  cmpfi  23522  filconn  23997  ufprim  24023  ufildr  24045  alexsubALTlem2  24162  alexsubALTlem3  24163  alexsubALTlem4  24164  ovolicc2lem3  25635  rolle  26106  dvivthlem1  26124  coeaddlem  26363  dgrco  26389  plymul0or  26396  aalioulem3  26452  cxpge0  26802  cxpmul2z  26810  cxpcn3lem  26866  scvxcvx  27104  sqf11  27257  ppiublem1  27320  lgsdir2lem2  27444  lgsqrlem2  27465  2sqnn0  27556  2sqnn  27557  nosepon  27783  nolesgn2ores  27790  nogesgn1ores  27792  nosepne  27798  nolt02o  27813  nosupbnd1lem5  27830  madebdaylemlrcut  28046  madebday  28047  ltslpss  28055  addsproplem2  28117  leadds1  28136  addsuniflem  28148  mulsproplem9  28271  sltmuls1  28294  sltmuls2  28295  muls0ord  28332  precsexlem9  28362  precsexlem11  28364  recsex  28366  abssnid  28390  ltonold  28408  onnolt  28413  eucliddivs  28523  elnnzs  28548  expsne0  28583  bdaypw2n0bndlem  28610  bdayfinbndlem1  28614  z12zsodd  28629  lmieu  29032  upgrpredgv  29394  edglnl  29398  eucrct2eupth  30501  frgrogt3nreg  30653  nvmul0or  30907  hvmul0or  31282  snsssng  32766  disjxpin  32839  expgt0b  33069  axprALT2  35412  subfacp1lem4  35541  satfvsucsuc  35723  satfrnmapom  35728  sat1el2xp  35737  gonarlem  35752  gonar  35753  goalrlem  35754  goalr  35755  fmlasucdisj  35757  satffunlem1lem1  35760  satffunlem2lem1  35762  untsucf  36068  dfon2lem6  36144  broutsideof2  36480  btwnoutside  36483  broutsideof3  36484  outsideoftr  36487  lineunray  36505  lineelsb2  36506  finminlem  36686  nn0prpw  36691  refssfne  36726  meran1  36779  ontgval  36799  ordcmp  36815  axtcond  36846  mh-inf3f1  36909  bj-sngltag  37475  bj-axseprep  37566  bj-prmoore  37612  topdifinfindis  37847  icoreclin  37858  rdgssun  37879  finxpsuclem  37898  poimirlem24  38150  poimirlem25  38151  poimirlem29  38155  poimirlem31  38157  mblfinlem2  38164  ovoliunnfl  38168  itg2addnclem  38177  sdclem2  38248  fdc  38251  divrngidl  38534  lkreqN  39801  cvrnbtwn4  39910  4atlem12  40243  elpaddn0  40431  paddasslem17  40467  paddidm  40472  pmapjoin  40483  llnexchb2  40500  dalawlem13  40514  dalawlem14  40515  dochkrshp4  42020  lcfl6  42131  lcmineqlem  42676  primrootspoweq0  42730  aks6d1c1  42740  sticksstones22  42792  aks6d1c6lem3  42796  oexpreposd  42938  expeqidd  42941  sn-remul0ord  43024  sn-sup2  43120  fphpdo  43401  pellfundex  43470  jm2.19lem4  43576  jm2.26a  43584  ordnexbtwnsuc  43851  onov0suclim  43858  oege2  43891  succlg  43912  dflim5  43913  oacl2g  43914  omcl2  43917  omcl3g  43918  naddgeoa  43978  safesnsupfiss  43998  fzunt  44038  fzuntd  44039  fzunt1d  44040  fzuntgd  44041  relexpmulg  44293  relexp01min  44296  relexpxpmin  44300  relexpaddss  44301  clsk1indlem3  44626  or2expropbi  47627  ich2exprop  48076  poprelb  48129  reuopreuprim  48131  goldbachthlem2  48154  nprmdvdsfacm1lem2  48229  nprmdvdsfacm1  48232  requad01  48242  evenltle  48338  gbowge7  48384  bgoldbtbndlem3  48428  elclnbgrelnbgr  48446  clnbgrel  48449  dfclnbgr6  48477  dfnbgr6  48478  dfsclnbgr6  48479  upgrimpths  48530  clnbgrgrim  48555  isubgr3stgrlem4  48590  isubgr3stgrlem7  48593  grlimgredgex  48621  gpgedgvtx1  48683  gpgvtxedg0  48684  gpgvtxedg1  48685  lidldomn1  48852  uzlidlring  48856  prelrrx2b  49346  line2y  49387  itschlc0xyqsol1  49398  itsclc0xyqsolr  49401  inlinecirc02plem  49418