Theorem jaod 858

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

Syntax hints:   → wi 4   ∨ wo 846

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 207  df-or 847

This theorem is referenced by:  mpjaod  859  orel2  889  pm2.621  897  pm2.63  941  jaao  955  jaodan  958  ecase2dOLD  1031  ecase3d  1034  dedlema  1046  dedlemb  1047  cad0  1615  cad0OLD  1616  psssstr  4132  eqoreldif  4708  opthpr  4876  prel12g  4888  opthprneg  4889  sotric  5637  sotr2  5641  sotr3  5648  relop  5875  suctr  6481  trsucss  6483  ordelinel  6496  fununi  6653  fnprb  7245  soisoi  7364  ordunisuc2  7881  poxp  8169  soxp  8170  frrlem12  8338  frrlem13  8339  wfrlem14OLD  8378  wfrlem15OLD  8379  tfrlem11  8444  omordi  8622  om00  8631  odi  8635  omeulem2  8639  oewordi  8647  nnmordi  8687  omsmolem  8713  swoord2  8796  nneneq  9272  nneneqOLD  9284  dffi3  9500  inf3lem6  9702  cantnfle  9740  cantnflem1  9758  cantnflem2  9759  ttrcltr  9785  r1sdom  9843  r1ord3g  9848  rankxplim3  9950  carddom2  10046  wdomnumr  10133  alephordi  10143  alephdom  10150  cardaleph  10158  djuinf  10258  cfsuc  10326  cfsmolem  10339  sornom  10346  fin23lem25  10393  fin1a2lem11  10479  fin1a2s  10483  zorn2lem7  10571  ttukeylem5  10582  alephval2  10641  fpwwe2lem12  10711  gch2  10744  gchaclem  10747  prub  11063  sqgt0sr  11175  1re  11290  lelttr  11380  ltletr  11382  letr  11384  mul0or  11930  prodgt0  12141  mulge0b  12165  squeeze0  12198  sup2  12251  un0addcl  12586  un0mulcl  12587  nn0sub  12603  elnnz  12649  zindd  12744  rpneg  13089  xrlttri  13201  xrlelttr  13218  xrltletr  13219  xrletr  13220  qextlt  13265  qextle  13266  xmullem2  13327  xlemul1a  13350  xrsupexmnf  13367  xrinfmexpnf  13368  supxrun  13378  prunioo  13541  difreicc  13544  iccsplit  13545  uzsplit  13656  fzm1  13664  expcl2lem  14124  expeq0  14143  expnegz  14147  expaddz  14157  expmulz  14159  sqlecan  14258  facdiv  14336  facwordi  14338  bcpasc  14370  resqrex  15299  absexpz  15354  caubnd  15407  summo  15765  zsum  15766  zprod  15985  rpnnen2lem12  16273  ordvdsmul  16348  nn0rppwr  16608  nn0expgcd  16611  dvdsprime  16734  2mulprm  16740  ge2nprmge4  16748  prmdvdsexpr  16764  prmfac1  16767  pythagtriplem2  16864  4sqlem11  17002  vdwlem6  17033  vdwlem9  17036  vdwlem13  17040  cshwshashlem3  17145  prmlem0  17153  pleval2  18407  pltletr  18413  plelttr  18414  tsrlemax  18656  smndex1mgm  18942  f1omvdco2  19490  psgnunilem2  19537  efgredlemc  19787  frgpuptinv  19813  lt6abl  19937  dmdprdsplit2lem  20089  domneq0  20730  drngmul0orOLD  20783  lvecvs0or  21133  baspartn  22982  0top  23011  indistopon  23029  restntr  23211  cnindis  23321  cmpfi  23437  filconn  23912  ufprim  23938  ufildr  23960  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  ovolicc2lem3  25573  rolle  26048  dvivthlem1  26067  coeaddlem  26308  dgrco  26335  plymul0or  26340  aalioulem3  26394  cxpge0  26743  cxpmul2z  26751  cxpcn3lem  26808  scvxcvx  27047  sqf11  27200  ppiublem1  27264  lgsdir2lem2  27388  lgsqrlem2  27409  2sqnn0  27500  2sqnn  27501  nosepon  27728  nolesgn2ores  27735  nogesgn1ores  27737  nosepne  27743  nolt02o  27758  nosupbnd1lem5  27775  madebdaylemlrcut  27955  madebday  27956  sltlpss  27963  addsproplem2  28021  sleadd1  28040  addsuniflem  28052  mulsproplem9  28168  ssltmul1  28191  ssltmul2  28192  muls0ord  28229  precsexlem9  28257  precsexlem11  28259  recsex  28261  abssnid  28285  sltonold  28301  elnnzs  28405  expsne0  28432  zs12bday  28442  lmieu  28810  upgrpredgv  29174  edglnl  29178  eucrct2eupth  30277  frgrogt3nreg  30429  nvmul0or  30682  hvmul0or  31057  snsssng  32543  disjxpin  32610  expgt0b  32820  subfacp1lem4  35151  satfvsucsuc  35333  satfrnmapom  35338  sat1el2xp  35347  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  untsucf  35672  dfon2lem6  35752  broutsideof2  36086  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  lineunray  36111  lineelsb2  36112  finminlem  36284  nn0prpw  36289  refssfne  36324  meran1  36377  ontgval  36397  ordcmp  36413  bj-sngltag  36949  bj-prmoore  37081  topdifinfindis  37312  icoreclin  37323  rdgssun  37344  finxpsuclem  37363  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  mblfinlem2  37618  ovoliunnfl  37622  itg2addnclem  37631  sdclem2  37702  fdc  37705  divrngidl  37988  lkreqN  39126  cvrnbtwn4  39235  4atlem12  39569  elpaddn0  39757  paddasslem17  39793  paddidm  39798  pmapjoin  39809  llnexchb2  39826  dalawlem13  39840  dalawlem14  39841  dochkrshp4  41346  lcfl6  41457  lcmineqlem  42009  primrootspoweq0  42063  aks6d1c1  42073  sticksstones22  42125  aks6d1c6lem3  42129  oexpreposd  42309  expeqidd  42312  sn-sup2  42447  fphpdo  42773  pellfundex  42842  jm2.19lem4  42949  jm2.26a  42957  ordnexbtwnsuc  43229  onov0suclim  43236  oege2  43269  succlg  43290  dflim5  43291  oacl2g  43292  omcl2  43295  omcl3g  43296  naddgeoa  43356  safesnsupfiss  43377  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  relexpaddss  43680  clsk1indlem3  44005  or2expropbi  46949  ich2exprop  47345  poprelb  47398  reuopreuprim  47400  goldbachthlem2  47420  requad01  47495  evenltle  47591  gbowge7  47637  bgoldbtbndlem3  47681  clnbgrel  47701  dfclnbgr6  47728  dfnbgr6  47729  dfsclnbgr6  47730  clnbgrgrim  47786  lidldomn1  47954  uzlidlring  47958  prelrrx2b  48448  line2y  48489  itschlc0xyqsol1  48500  itsclc0xyqsolr  48503  inlinecirc02plem  48520