Theorem jaod 873

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  mpjaod  874  orel2  904  pm2.621  912  pm2.63  955  jaao  969  jaodan  972  ecase3d  1050  dedlema  1061  dedlemb  1062  cad0  1651  psssstr  4058  eqoreldif  4646  opthpr  4811  prel12g  4824  opthprneg  4825  axpr  5392  sotric  5593  sotr2  5597  sotr3  5604  relop  5830  suctr  6446  trsucss  6448  ordelinel  6461  fununi  6608  fnprb  7207  soisoi  7329  ordunisuc2  7840  poxp  8126  soxp  8127  frrlem12  8296  frrlem13  8297  tfrlem11  8377  omordi  8553  om00  8562  odi  8566  omeulem2  8570  oewordi  8579  nnmordi  8619  omsmolem  8645  swoord2  8730  nneneq  9200  dffi3  9401  inf3lem6  9612  cantnfle  9650  cantnflem1  9668  cantnflem2  9669  ttrcltr  9695  r1sdom  9756  r1ord3g  9761  rankxplim3  9863  carddom2  9982  wdomnumr  10067  alephordi  10077  alephdom  10084  cardaleph  10092  djuinf  10191  cfsuc  10259  cfsmolem  10272  sornom  10279  fin23lem25  10326  fin1a2lem11  10412  fin1a2s  10416  zorn2lem7  10504  ttukeylem5  10515  alephval2  10581  fpwwe2lem12  10651  gch2  10684  gchaclem  10687  prub  11003  sqgt0sr  11115  1re  11232  lelttr  11324  ltletr  11326  letr  11328  mul0or  11878  prodgt0  12086  mulge0b  12109  squeeze0  12142  sup2  12195  un0addcl  12561  un0mulcl  12562  nn0sub  12578  elnnz  12625  zindd  12722  rpneg  13076  xrlttri  13190  xrlelttr  13207  xrltletr  13208  xrletr  13209  qextlt  13255  qextle  13256  xmullem2  13317  xlemul1a  13340  xrsupexmnf  13357  xrinfmexpnf  13358  supxrun  13368  prunioo  13534  difreicc  13537  iccsplit  13538  uzsplit  13651  fzm1  13662  expcl2lem  14137  expeq0  14156  expnegz  14160  expaddz  14170  expmulz  14172  sqlecan  14273  facdiv  14351  facwordi  14353  bcpasc  14385  resqrex  15337  absexpz  15392  caubnd  15446  summo  15803  zsum  15804  zprod  16024  rpnnen2lem12  16313  ordvdsmul  16390  nn0rppwr  16651  nn0expgcd  16654  dvdsprime  16777  2mulprm  16783  ge2nprmge4  16792  prmdvdsexpr  16808  prmfac1  16811  pythagtriplem2  16909  4sqlem11  17047  vdwlem6  17078  vdwlem9  17081  vdwlem13  17085  cshwshashlem3  17189  prmlem0  17197  pleval2  18423  pltletr  18429  plelttr  18430  tsrlemax  18674  smndex1mgm  19019  f1omvdco2  19575  psgnunilem2  19622  efgredlemc  19872  frgpuptinv  19898  lt6abl  20022  dmdprdsplit2lem  20174  domneq0  20870  lvecvs0or  21295  unichnlidl  21425  baspartn  23179  0top  23208  indistopon  23226  restntr  23407  cnindis  23517  cmpfi  23633  filconn  24109  ufprim  24135  ufildr  24157  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALTlem4  24276  ovolicc2lem3  25747  rolle  26217  dvivthlem1  26235  coeaddlem  26475  dgrco  26501  plymul0or  26508  aalioulem3  26570  cxpge0  26920  cxpmul2z  26928  cxpcn3lem  26984  scvxcvx  27222  sqf11  27375  ppiublem1  27438  lgsdir2lem2  27562  lgsqrlem2  27583  2sqnn0  27674  2sqnn  27675  nosepon  27901  nolesgn2ores  27908  nogesgn1ores  27910  nosepne  27916  nolt02o  27931  nosupbnd1lem5  27948  madebdaylemlrcut  28164  madebday  28165  ltslpss  28173  addsproplem2  28235  leadds1  28254  addsuniflem  28266  mulsproplem9  28389  sltmuls1  28412  sltmuls2  28413  muls0ord  28450  precsexlem9  28480  precsexlem11  28482  recsex  28484  abssnid  28508  ltonold  28526  onnolt  28531  eucliddivs  28641  elnnzs  28666  expsne0  28701  bdaypw2n0bndlem  28728  bdayfinbndlem1  28732  z12zsodd  28747  lmieu  29168  upgrpredgv  29596  edglnl  29600  eucrct2eupth  30725  frgrogt3nreg  30877  nvmul0or  31131  hvmul0or  31506  snsssng  32989  disjxpin  33061  expgt0b  33287  axprALT2  35617  subfacp1lem4  35762  satfvsucsuc  35944  satfrnmapom  35949  sat1el2xp  35958  gonarlem  35973  gonar  35974  goalrlem  35975  goalr  35976  fmlasucdisj  35978  satffunlem1lem1  35981  satffunlem2lem1  35983  untsucf  36289  dfon2lem6  36365  broutsideof2  36702  btwnoutside  36705  broutsideof3  36706  outsideoftr  36709  lineunray  36727  lineelsb2  36728  nmuladdss  36793  ltnadd  36798  nadddilem4  36803  finminlem  36937  nn0prpw  36942  refssfne  36977  meran1  37030  ontgval  37050  ordcmp  37066  axtcond  37097  mh-inf3f1  37160  bj-sngltag  37727  bj-axseprep  37819  bj-prmoore  37865  topdifinfindis  38100  icoreclin  38111  rdgssun  38132  finxpsuclem  38151  poimirlem24  38393  poimirlem25  38394  poimirlem29  38398  poimirlem31  38400  mblfinlem2  38407  ovoliunnfl  38411  itg2addnclem  38420  sdclem2  38492  fdc  38495  divrngidl  38778  lkreqN  40043  cvrnbtwn4  40152  4atlem12  40485  elpaddn0  40673  paddasslem17  40709  paddidm  40714  pmapjoin  40725  llnexchb2  40742  dalawlem13  40756  dalawlem14  40757  dochkrshp4  42262  lcfl6  42373  lcmineqlem  42918  primrootspoweq0  42972  aks6d1c1  42982  sticksstones22  43034  aks6d1c6lem3  43038  oexpreposd  43197  expeqidd  43200  sn-remul0ord  43283  sn-sup2  43379  fphpdo  43658  pellfundex  43727  jm2.19lem4  43833  jm2.26a  43841  ordnexbtwnsuc  44108  onov0suclim  44115  oege2  44148  succlg  44169  dflim5  44170  oacl2g  44171  omcl2  44174  omcl3g  44175  naddgeoa  44235  safesnsupfiss  44255  fzunt  44295  fzuntd  44296  fzunt1d  44297  fzuntgd  44298  relexpmulg  44550  relexp01min  44553  relexpxpmin  44557  relexpaddss  44558  clsk1indlem3  44883  or2expropbi  47922  ich2exprop  48371  poprelb  48424  reuopreuprim  48426  goldbachthlem2  48449  nprmdvdsfacm1lem2  48524  nprmdvdsfacm1  48527  requad01  48537  evenltle  48633  gbowge7  48679  bgoldbtbndlem3  48723  elclnbgrelnbgr  48741  clnbgrel  48744  dfclnbgr6  48772  dfnbgr6  48773  dfsclnbgr6  48774  upgrimpths  48825  clnbgrgrim  48850  isubgr3stgrlem4  48885  isubgr3stgrlem7  48888  grlimgredgex  48916  gpgedgvtx1  48978  gpgvtxedg0  48979  gpgvtxedg1  48980  lidldomn1  49146  uzlidlring  49150  prelrrx2b  49644  line2y  49685  itschlc0xyqsol1  49696  itsclc0xyqsolr  49699  inlinecirc02plem  49716