Theorem mp3an1 1450

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an1.1	⊢ 𝜑
mp3an1.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 690	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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-an 396  df-3an 1088

This theorem is referenced by:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7723  tfrlem9  8304  oaord1  8466  oaword2  8468  oawordeulem  8469  oa00  8474  omword1  8488  omword2  8489  omlimcl  8493  oeoelem  8513  nnaordex  8553  naddword1  8606  undom  8978  sucdom2  9112  fodomfi  9196  fodomfib  9213  dffi3  9315  unbnn3  9549  ttrcltr  9606  frmin  9642  frrlem16  9651  pwdjuen  10073  zorn2  10397  zornn0  10399  ttukey  10409  brdom7disj  10422  brdom6disj  10423  muladd11  11283  negsubdi  11417  mulneg1  11553  ltaddpos  11607  addge01  11627  reccl  11783  recid  11790  recid2  11791  div0  11809  recdiv2  11834  divdiv23zi  11874  ltmul12a  11977  lemul12a  11979  mulgt1OLD  11980  ltmulgt11  11981  gt0div  11988  ge0div  11989  lediv12a  12015  ledivp1  12024  ltdiv23i  12046  ledivp1i  12047  ltdivp1i  12048  infm3  12081  8th4div3  12341  gtndiv  12550  nn0ind  12568  xrre2  13069  2resupmax  13087  qsqueeze  13100  xmulpnf1  13173  xlemul1a  13187  ioorebas  13351  elfz0ubfz0  13532  le2sq2  14042  expubnd  14085  crreczi  14135  bccl  14229  hashbc  14360  wrdred1hash  14468  ccatlid  14494  shftfval  14977  sgnp  14997  sqreulem  15267  binom1p  15738  fallrisefac  15932  efsub  16009  efi4p  16046  sinadd  16073  cosadd  16074  demoivreALT  16110  rpnnen2lem4  16126  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  divalglem4  16307  divalglem9  16312  gcdcllem3  16412  gcdadd  16437  algcvgblem  16488  isprm3  16594  1arith2  16840  vdwap0  16888  vdwap1  16889  ipolt  18441  smndex1sgrp  18816  f1otrspeq  19359  rmodislmod  20863  cnfldneg  21332  cnflddiv  21337  cnflddivOLD  21338  cnfldmulg  21340  cnfldexp  21341  zringsub  21392  zringmulg  21393  zringsubgval  21407  remulg  21544  resubgval  21546  thlleval  21635  mplsubrglem  21941  evls1rhm  22237  iccordt  23129  bl2ioo  24707  xrsblre  24727  iccntr  24737  icccmplem3  24740  reconnlem2  24743  opnreen  24747  mpomulcn  24785  iccpnfcnv  24869  cnllycmp  24882  pcoptcl  24948  ismbl2  25455  cmmbl  25462  nulmbl  25463  unmbl  25465  voliunlem2  25479  ioombl1  25490  opnmbllem  25529  mbfima  25558  ellimc3  25807  limcflf  25809  coe1termlem  26190  dvnply2  26222  dvnply  26223  reeff1o  26384  sinperlem  26416  resinf1o  26472  logeftb  26519  logge0  26541  efopn  26594  loglesqrt  26698  logrec  26700  xrlimcnp  26905  ppinncl  27111  chtrpcl  27112  bposlem2  27223  bposlem8  27229  lgsdir2  27268  1lgs  27278  nosupno  27642  nosupbday  27644  noinfno  27657  noinfbday  27659  noetasuplem4  27675  lrrecfr  27886  sltmul  28075  ax5seglem2  28907  axcontlem2  28943  fusgrfis  29308  3cyclfrgrrn  30266  isgrpoi  30478  imsmetlem  30670  nmcvcn  30675  ipval2  30687  lnocoi  30737  nmlno0lem  30773  nmblolbii  30779  blometi  30783  blocnilem  30784  blocni  30785  ipasslem1  30811  ipasslem2  30812  ipasslem4  30814  ipasslem5  30815  ipasslem8  30817  ipblnfi  30835  ip2eqi  30836  ubthlem1  30850  htthlem  30897  h2hmetdval  30958  axhvcom-zf  30963  axhis1-zf  30974  axhis4-zf  30977  hvm1neg  31012  hvsub4  31017  hvsubass  31024  hvsubdistr2  31030  hv2times  31041  hvsubcan  31054  hvsubcan2  31055  his2sub  31072  norm-i  31109  normpyc  31126  hhip  31157  hhph  31158  norm1exi  31230  hhssabloilem  31241  hhssnv  31244  hhshsslem2  31248  hhssmetdval  31257  shscli  31297  shunssi  31348  shsleji  31350  shsidmi  31364  spanunsni  31559  h1datomi  31561  spansncvi  31632  pjss2i  31660  pjssmii  31661  pjocini  31678  homullid  31780  honegdi  31789  ho2times  31799  nmopge0  31891  nmopgt0  31892  nmfnge0  31907  lnopaddi  31951  lnopmuli  31952  lnopsubi  31954  hmopbdoptHIL  31968  nmbdoplbi  32004  nmcoplbi  32008  nmophmi  32011  lnopconi  32014  lnfnaddi  32023  lnfnsubi  32026  nmbdfnlbi  32029  nmcfnlbi  32032  lnfnconi  32035  imaelshi  32038  cnlnadjlem2  32048  cnlnadjlem7  32053  nmoptrii  32074  nmopcoi  32075  adjcoi  32080  nmopcoadji  32081  bracnlnval  32094  leopmul  32114  opsqrlem1  32120  opsqrlem6  32125  hmopidmpji  32132  sto2i  32217  strlem1  32230  atcveq0  32328  atcv0eq  32359  atomli  32362  atcvati  32366  atcvat3i  32376  cdjreui  32412  cdj1i  32413  xdiv0  32909  xdivpnfrp  32913  mhmhmeotmd  33940  rezh  33982  qqhucn  34005  blsconn  35288  cnllysconn  35289  sate0fv0  35461  prv0  35474  sinccvglem  35716  opnrebl2  36365  ptrecube  37659  poimirlem6  37665  poimirlem7  37666  poimirlem29  37688  poimirlem30  37689  opnmbllem0  37695  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  voliunnfl  37703  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  heiborlem7  37856  rrnequiv  37874  ismrer1  37877  el3v1  38264  preuniqval  38507  cnaddcom  39070  lcmineqlem1  42121  sn-ltaddpos  42545  mapco2  42807  mzpaddmpt  42833  mzpmulmpt  42834  zindbi  43038  mpaaeu  43242  tfsconcat0b  43438  eel000cT  44794  eel0TT  44795  supminfxr  45561  fmtno4prmfac  47671  pgn4cyclex  48225  aacllem  49901