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  4065  eqoreldif  4653  opthpr  4818  prel12g  4831  opthprneg  4832  axpr  5400  sotric  5601  sotr2  5605  sotr3  5612  relop  5838  suctr  6453  trsucss  6455  ordelinel  6468  fununi  6615  fnprb  7210  soisoi  7332  ordunisuc2  7842  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  9193  dffi3  9394  inf3lem6  9605  cantnfle  9643  cantnflem1  9661  cantnflem2  9662  ttrcltr  9688  r1sdom  9749  r1ord3g  9754  rankxplim3  9856  carddom2  9975  wdomnumr  10060  alephordi  10070  alephdom  10077  cardaleph  10085  djuinf  10184  cfsuc  10252  cfsmolem  10265  sornom  10272  fin23lem25  10319  fin1a2lem11  10405  fin1a2s  10409  zorn2lem7  10497  ttukeylem5  10508  alephval2  10568  fpwwe2lem12  10638  gch2  10671  gchaclem  10674  prub  10990  sqgt0sr  11102  1re  11219  lelttr  11311  ltletr  11313  letr  11315  mul0or  11865  prodgt0  12073  mulge0b  12096  squeeze0  12129  sup2  12182  un0addcl  12548  un0mulcl  12549  nn0sub  12565  elnnz  12612  zindd  12708  rpneg  13061  xrlttri  13175  xrlelttr  13192  xrltletr  13193  xrletr  13194  qextlt  13240  qextle  13241  xmullem2  13302  xlemul1a  13325  xrsupexmnf  13342  xrinfmexpnf  13343  supxrun  13353  prunioo  13519  difreicc  13522  iccsplit  13523  uzsplit  13636  fzm1  13647  expcl2lem  14122  expeq0  14141  expnegz  14145  expaddz  14155  expmulz  14157  sqlecan  14258  facdiv  14336  facwordi  14338  bcpasc  14370  resqrex  15320  absexpz  15375  caubnd  15429  summo  15786  zsum  15787  zprod  16009  rpnnen2lem12  16298  ordvdsmul  16375  nn0rppwr  16636  nn0expgcd  16639  dvdsprime  16762  2mulprm  16768  ge2nprmge4  16777  prmdvdsexpr  16793  prmfac1  16796  pythagtriplem2  16894  4sqlem11  17032  vdwlem6  17063  vdwlem9  17066  vdwlem13  17070  cshwshashlem3  17174  prmlem0  17182  pleval2  18408  pltletr  18414  plelttr  18415  tsrlemax  18659  smndex1mgm  18992  f1omvdco2  19541  psgnunilem2  19588  efgredlemc  19838  frgpuptinv  19864  lt6abl  19988  dmdprdsplit2lem  20140  domneq0  20836  lvecvs0or  21261  unichnlidl  21391  baspartn  23140  0top  23169  indistopon  23187  restntr  23368  cnindis  23478  cmpfi  23594  filconn  24069  ufprim  24095  ufildr  24117  alexsubALTlem2  24234  alexsubALTlem3  24235  alexsubALTlem4  24236  ovolicc2lem3  25707  rolle  26178  dvivthlem1  26196  coeaddlem  26435  dgrco  26461  plymul0or  26468  aalioulem3  26526  cxpge0  26877  cxpmul2z  26885  cxpcn3lem  26941  scvxcvx  27179  sqf11  27332  ppiublem1  27395  lgsdir2lem2  27519  lgsqrlem2  27540  2sqnn0  27631  2sqnn  27632  nosepon  27858  nolesgn2ores  27865  nogesgn1ores  27867  nosepne  27873  nolt02o  27888  nosupbnd1lem5  27905  madebdaylemlrcut  28121  madebday  28122  ltslpss  28130  addsproplem2  28192  leadds1  28211  addsuniflem  28223  mulsproplem9  28346  sltmuls1  28369  sltmuls2  28370  muls0ord  28407  precsexlem9  28437  precsexlem11  28439  recsex  28441  abssnid  28465  ltonold  28483  onnolt  28488  eucliddivs  28598  elnnzs  28623  expsne0  28658  bdaypw2n0bndlem  28685  bdayfinbndlem1  28689  z12zsodd  28704  lmieu  29122  upgrpredgv  29518  edglnl  29522  eucrct2eupth  30625  frgrogt3nreg  30777  nvmul0or  31031  hvmul0or  31406  snsssng  32889  disjxpin  32962  expgt0b  33190  axprALT2  35520  subfacp1lem4  35688  satfvsucsuc  35870  satfrnmapom  35875  sat1el2xp  35884  gonarlem  35899  gonar  35900  goalrlem  35901  goalr  35902  fmlasucdisj  35904  satffunlem1lem1  35907  satffunlem2lem1  35909  untsucf  36215  dfon2lem6  36291  broutsideof2  36627  btwnoutside  36630  broutsideof3  36631  outsideoftr  36634  lineunray  36652  lineelsb2  36653  nmuladdss  36718  ltnadd  36723  nadddilem4  36728  finminlem  36862  nn0prpw  36867  refssfne  36902  meran1  36955  ontgval  36975  ordcmp  36991  axtcond  37022  mh-inf3f1  37085  bj-sngltag  37652  bj-axseprep  37744  bj-prmoore  37790  topdifinfindis  38025  icoreclin  38036  rdgssun  38057  finxpsuclem  38076  poimirlem24  38328  poimirlem25  38329  poimirlem29  38333  poimirlem31  38335  mblfinlem2  38342  ovoliunnfl  38346  itg2addnclem  38355  sdclem2  38426  fdc  38429  divrngidl  38712  lkreqN  39977  cvrnbtwn4  40086  4atlem12  40419  elpaddn0  40607  paddasslem17  40643  paddidm  40648  pmapjoin  40659  llnexchb2  40676  dalawlem13  40690  dalawlem14  40691  dochkrshp4  42196  lcfl6  42307  lcmineqlem  42852  primrootspoweq0  42906  aks6d1c1  42916  sticksstones22  42968  aks6d1c6lem3  42972  oexpreposd  43116  expeqidd  43119  sn-remul0ord  43202  sn-sup2  43298  fphpdo  43577  pellfundex  43646  jm2.19lem4  43752  jm2.26a  43760  ordnexbtwnsuc  44027  onov0suclim  44034  oege2  44067  succlg  44088  dflim5  44089  oacl2g  44090  omcl2  44093  omcl3g  44094  naddgeoa  44154  safesnsupfiss  44174  fzunt  44214  fzuntd  44215  fzunt1d  44216  fzuntgd  44217  relexpmulg  44469  relexp01min  44472  relexpxpmin  44476  relexpaddss  44477  clsk1indlem3  44802  or2expropbi  47804  ich2exprop  48253  poprelb  48306  reuopreuprim  48308  goldbachthlem2  48331  nprmdvdsfacm1lem2  48406  nprmdvdsfacm1  48409  requad01  48419  evenltle  48515  gbowge7  48561  bgoldbtbndlem3  48605  elclnbgrelnbgr  48623  clnbgrel  48626  dfclnbgr6  48654  dfnbgr6  48655  dfsclnbgr6  48656  upgrimpths  48707  clnbgrgrim  48732  isubgr3stgrlem4  48767  isubgr3stgrlem7  48770  grlimgredgex  48798  gpgedgvtx1  48860  gpgvtxedg0  48861  gpgvtxedg1  48862  lidldomn1  49029  uzlidlring  49033  prelrrx2b  49527  line2y  49568  itschlc0xyqsol1  49579  itsclc0xyqsolr  49582  inlinecirc02plem  49599