Theorem mp3an1 1447

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 687	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  mp3an12  1450  mp3an1i  1453  mp3anl1  1454  mp3an  1460  mp3an2i  1465  mp3an3an  1466  onint  7649  wfrlem12OLD  8160  tfrlem9  8225  oaord1  8391  oaword2  8393  oawordeulem  8394  oa00  8399  omword1  8413  omword2  8414  omlimcl  8418  oeoelem  8438  nnaordex  8478  undom  8855  rexdif1en  8953  sucdom2  8998  enp1i  9061  dffi3  9199  unbnn3  9426  ttrcltr  9483  frmin  9516  frrlem16  9525  pwdjuen  9946  zorn2  10271  zornn0  10273  ttukey  10283  brdom7disj  10296  brdom6disj  10297  muladd11  11154  negsubdi  11286  mulneg1  11420  ltaddpos  11474  addge01  11494  reccl  11649  recid  11656  recid2  11657  recdiv2  11697  divdiv23zi  11737  ltmul12a  11840  lemul12a  11842  mulgt1  11843  ltmulgt11  11844  gt0div  11850  ge0div  11851  lediv12a  11877  ledivp1  11886  ltdiv23i  11908  ledivp1i  11909  ltdivp1i  11910  infm3  11943  8th4div3  12202  gtndiv  12406  nn0ind  12424  xrre2  12913  2resupmax  12931  qsqueeze  12944  xmulpnf1  13017  xlemul1a  13031  ioorebas  13192  elfz0ubfz0  13369  le2sq2  13863  expubnd  13904  crreczi  13952  bccl  14045  hashbc  14174  wrdred1hash  14273  ccatlid  14300  shftfval  14790  sgnp  14810  sqreulem  15080  binom1p  15552  fallrisefac  15744  efsub  15818  efi4p  15855  sinadd  15882  cosadd  15883  demoivreALT  15919  rpnnen2lem4  15935  odd2np1  16059  opoe  16081  omoe  16082  opeo  16083  omeo  16084  divalglem4  16114  divalglem9  16119  gcdcllem3  16217  gcdadd  16242  algcvgblem  16291  isprm3  16397  1arith2  16638  vdwap0  16686  vdwap1  16687  ipolt  18262  smndex1sgrp  18556  f1otrspeq  19064  rmodislmod  20200  rmodislmodOLD  20201  cnfldneg  20633  cnflddiv  20637  cnfldmulg  20639  cnfldexp  20640  zringmulg  20687  zringsubgval  20701  remulg  20821  resubgval  20823  thlleval  20914  mplsubrglem  21219  evls1rhm  21497  iccordt  22374  bl2ioo  23964  xrsblre  23983  iccntr  23993  icccmplem3  23996  reconnlem2  23999  opnreen  24003  iccpnfcnv  24116  cnllycmp  24128  pcoptcl  24193  ismbl2  24700  cmmbl  24707  nulmbl  24708  unmbl  24710  voliunlem2  24724  ioombl1  24735  opnmbllem  24774  mbfima  24803  ellimc3  25052  limcflf  25054  coe1termlem  25428  dvnply2  25456  dvnply  25457  reeff1o  25615  sinperlem  25646  resinf1o  25701  logeftb  25748  logge0  25769  efopn  25822  loglesqrt  25920  logrec  25922  xrlimcnp  26127  ppinncl  26332  chtrpcl  26333  bposlem2  26442  bposlem8  26448  lgsdir2  26487  1lgs  26497  ax5seglem2  27306  axcontlem2  27342  fusgrfis  27706  3cyclfrgrrn  28659  isgrpoi  28869  imsmetlem  29061  nmcvcn  29066  ipval2  29078  lnocoi  29128  nmlno0lem  29164  nmblolbii  29170  blometi  29174  blocnilem  29175  blocni  29176  ipasslem1  29202  ipasslem2  29203  ipasslem4  29205  ipasslem5  29206  ipasslem8  29208  ipblnfi  29226  ip2eqi  29227  ubthlem1  29241  htthlem  29288  h2hmetdval  29349  axhvcom-zf  29354  axhis1-zf  29365  axhis4-zf  29368  hvm1neg  29403  hvsub4  29408  hvsubass  29415  hvsubdistr2  29421  hv2times  29432  hvsubcan  29445  hvsubcan2  29446  his2sub  29463  norm-i  29500  normpyc  29517  hhip  29548  hhph  29549  norm1exi  29621  hhssabloilem  29632  hhssnv  29635  hhshsslem2  29639  hhssmetdval  29648  shscli  29688  shunssi  29739  shsleji  29741  shsidmi  29755  spanunsni  29950  h1datomi  29952  spansncvi  30023  pjss2i  30051  pjssmii  30052  pjocini  30069  homulid2  30171  honegdi  30180  ho2times  30190  nmopge0  30282  nmopgt0  30283  nmfnge0  30298  lnopaddi  30342  lnopmuli  30343  lnopsubi  30345  hmopbdoptHIL  30359  nmbdoplbi  30395  nmcoplbi  30399  nmophmi  30402  lnopconi  30405  lnfnaddi  30414  lnfnsubi  30417  nmbdfnlbi  30420  nmcfnlbi  30423  lnfnconi  30426  imaelshi  30429  cnlnadjlem2  30439  cnlnadjlem7  30444  nmoptrii  30465  nmopcoi  30466  adjcoi  30471  nmopcoadji  30472  bracnlnval  30485  leopmul  30505  opsqrlem1  30511  opsqrlem6  30516  hmopidmpji  30523  sto2i  30608  strlem1  30621  atcveq0  30719  atcv0eq  30750  atomli  30753  atcvati  30757  atcvat3i  30767  cdjreui  30803  cdj1i  30804  xdiv0  31212  xdivpnfrp  31216  mhmhmeotmd  31886  rezh  31930  qqhucn  31951  blsconn  33215  cnllysconn  33216  sate0fv0  33388  prv0  33401  sinccvglem  33639  nosupno  33915  nosupbday  33917  noinfno  33930  noinfbday  33932  noetasuplem4  33948  lrrecfr  34109  opnrebl2  34519  ptrecube  35786  poimirlem6  35792  poimirlem7  35793  poimirlem29  35815  poimirlem30  35816  opnmbllem0  35822  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  voliunnfl  35830  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  heiborlem7  35984  rrnequiv  36002  ismrer1  36005  el3v1  36381  cnaddcom  36993  lcmineqlem1  40044  2xp3dxp2ge1d  40169  sn-ltaddpos  40430  mapco2  40544  mzpaddmpt  40570  mzpmulmpt  40571  zindbi  40775  mpaaeu  40982  eel000cT  42330  eel0TT  42331  supminfxr  43011  fmtno4prmfac  45035  aacllem  46516