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  5389  sotric  5589  sotr2  5593  sotr3  5600  relop  5828  suctr  6450  trsucss  6452  ordelinel  6465  fununi  6613  fnprb  7212  soisoi  7334  ordunisuc2  7853  poxp  8138  soxp  8139  frrlem12  8308  frrlem13  8309  tfrlem11  8389  onelfvnef1  8442  omordi  8567  om00  8576  odi  8580  omeulem2  8584  oewordi  8593  nnmordi  8633  omsmolem  8659  swoord2  8744  nneneq  9214  dffi3  9416  inf3lem6  9627  cantnfle  9665  cantnflem1  9683  cantnflem2  9684  ttrcltr  9710  r1sdom  9774  r1ord3g  9779  rankxplim3  9891  carddom2  10051  wdomnumr  10136  alephordi  10146  alephdom  10153  cardaleph  10161  djuinf  10260  cfsuc  10328  cfsmolem  10341  sornom  10348  fin23lem25  10395  fin1a2lem11  10481  fin1a2s  10485  zorn2lem7  10573  ttukeylem5  10584  alephval2  10650  fpwwe2lem12  10720  gch2  10753  gchaclem  10756  prub  11072  sqgt0sr  11184  1re  11301  lelttr  11393  ltletr  11395  letr  11397  mul0or  11949  prodgt0  12157  mulge0b  12180  squeeze0  12213  sup2  12266  un0addcl  12632  un0mulcl  12633  nn0sub  12649  elnnz  12696  zindd  12793  rpneg  13147  xrlttri  13261  xrlelttr  13278  xrltletr  13279  xrletr  13280  qextlt  13326  qextle  13327  xmullem2  13388  xlemul1a  13411  xrsupexmnf  13428  xrinfmexpnf  13429  supxrun  13439  prunioo  13605  difreicc  13608  iccsplit  13609  uzsplit  13723  fzm1  13734  expcl2lem  14209  expeq0  14228  expnegz  14232  expaddz  14242  expmulz  14244  sqlecan  14346  facdiv  14424  facwordi  14426  bcpasc  14458  resqrex  15410  absexpz  15465  caubnd  15519  summo  15876  zsum  15877  zprod  16097  rpnnen2lem12  16386  ordvdsmul  16463  nn0rppwr  16728  nn0expgcd  16731  dvdsprime  16855  2mulprm  16861  ge2nprmge4  16870  prmdvdsexpr  16886  prmfac1  16889  pythagtriplem2  16988  4sqlem11  17126  vdwlem6  17157  vdwlem9  17160  vdwlem13  17164  cshwshashlem3  17268  prmlem0  17276  pleval2  18502  pltletr  18508  plelttr  18509  tsrlemax  18753  smndex1mgm  19099  f1omvdco2  19655  psgnunilem2  19702  efgredlemc  19952  frgpuptinv  19978  lt6abl  20102  dmdprdsplit2lem  20254  domneq0  20953  lvecvs0or  21379  unichnlidl  21509  baspartn  23265  0top  23294  indistopon  23312  restntr  23493  cnindis  23603  cmpfi  23719  filconn  24195  ufprim  24221  ufildr  24243  alexsubALTlem2  24360  alexsubALTlem3  24361  alexsubALTlem4  24362  ovolicc2lem3  25833  rolle  26303  dvivthlem1  26321  coeaddlem  26561  dgrco  26587  plymul0or  26592  aalioulem3  26654  cxpge0  27004  cxpmul2z  27012  cxpcn3lem  27068  scvxcvx  27306  sqf11  27459  ppiublem1  27522  lgsdir2lem2  27646  lgsqrlem2  27667  2sqnn0  27758  2sqnn  27759  fltoprmgt3  27989  nosepon  28015  nolesgn2ores  28022  nogesgn1ores  28024  nosepne  28030  nolt02o  28045  nosupbnd1lem5  28062  madebdaylemlrcut  28278  madebday  28279  ltslpss  28287  addsproplem2  28349  leadds1  28368  addsuniflem  28380  mulsproplem9  28503  sltmuls1  28526  sltmuls2  28527  muls0ord  28564  precsexlem9  28594  precsexlem11  28596  recsex  28598  abssnid  28622  ltonold  28640  onnolt  28645  eucliddivs  28755  elnnzs  28780  expsne0  28815  bdaypw2n0bndlem  28842  bdayfinbndlem1  28846  z12zsodd  28861  lmieu  29282  upgrpredgv  29710  edglnl  29714  eucrct2eupth  30839  frgrogt3nreg  30991  nvmul0or  31245  hvmul0or  31620  snsssng  33103  disjxpin  33175  expgt0b  33401  axprALT2  35723  subfacp1lem4  35927  satfvsucsuc  36109  satfrnmapom  36114  sat1el2xp  36123  gonarlem  36138  gonar  36139  goalrlem  36140  goalr  36141  fmlasucdisj  36143  satffunlem1lem1  36146  satffunlem2lem1  36148  untsucf  36454  dfon2lem6  36530  broutsideof2  36867  btwnoutside  36870  broutsideof3  36871  outsideoftr  36874  lineunray  36892  lineelsb2  36893  nmuladdss  36942  ltnadd  36947  nadddilem4  36952  finminlem  37086  nn0prpw  37091  refssfne  37126  meran1  37179  ontgval  37199  ordcmp  37215  axtcond  37246  bj-sngltag  37876  bj-axseprep  37970  bj-prmoore  38016  topdifinfindis  38249  icoreclin  38260  rdgssun  38281  finxpsuclem  38300  poimirlem24  38542  poimirlem25  38543  poimirlem29  38547  poimirlem31  38549  mblfinlem2  38556  ovoliunnfl  38560  itg2addnclem  38569  sdclem2  38656  fdc  38659  divrngidl  38942  lkreqN  40207  cvrnbtwn4  40316  4atlem12  40649  elpaddn0  40837  paddasslem17  40873  paddidm  40878  pmapjoin  40889  llnexchb2  40906  dalawlem13  40920  dalawlem14  40921  dochkrshp4  42426  lcfl6  42537  lcmineqlem  43082  primrootspoweq0  43136  aks6d1c1  43146  sticksstones22  43198  aks6d1c6lem3  43202  oexpreposd  43359  expeqidd  43362  sn-remul0ord  43439  sn-sup2  43535  fphpdo  43803  pellfundex  43872  jm2.19lem4  43978  jm2.26a  43986  ordnexbtwnsuc  44253  onov0suclim  44260  oege2  44293  succlg  44314  dflim5  44315  oacl2g  44316  omcl2  44319  omcl3g  44320  naddgeoa  44380  safesnsupfiss  44400  fzunt  44440  fzuntd  44441  fzunt1d  44442  fzuntgd  44443  relexpmulg  44695  relexp01min  44698  relexpxpmin  44702  relexpaddss  44703  clsk1indlem3  45028  or2expropbi  48073  ich2exprop  48522  poprelb  48575  reuopreuprim  48577  goldbachthlem2  48600  nprmdvdsfacm1lem2  48675  nprmdvdsfacm1  48678  requad01  48688  evenltle  48784  gbowge7  48830  bgoldbtbndlem3  48874  elclnbgrelnbgr  48892  clnbgrel  48895  dfclnbgr6  48923  dfnbgr6  48924  dfsclnbgr6  48925  upgrimpths  48976  clnbgrgrim  49001  isubgr3stgrlem4  49036  isubgr3stgrlem7  49039  grlimgredgex  49067  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  lidldomn1  49297  uzlidlring  49301  prelrrx2b  49795  line2y  49836  itschlc0xyqsol1  49847  itsclc0xyqsolr  49850  inlinecirc02plem  49867