Theorem mp3an1 1446

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

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

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

This theorem is referenced by:  mp3an12  1449  mp3an1i  1452  mp3anl1  1453  mp3an  1459  mp3an2i  1464  mp3an3an  1465  onint  7617  wfrlem12OLD  8122  tfrlem9  8187  oaord1  8344  oaword2  8346  oawordeulem  8347  oa00  8352  omword1  8366  omword2  8367  omlimcl  8371  oeoelem  8391  nnaordex  8431  rexdif1en  8906  enp1i  8982  dffi3  9120  unbnn3  9347  pwdjuen  9868  zorn2  10193  zornn0  10195  ttukey  10205  brdom7disj  10218  brdom6disj  10219  muladd11  11075  negsubdi  11207  mulneg1  11341  ltaddpos  11395  addge01  11415  reccl  11570  recid  11577  recid2  11578  recdiv2  11618  divdiv23zi  11658  ltmul12a  11761  lemul12a  11763  mulgt1  11764  ltmulgt11  11765  gt0div  11771  ge0div  11772  lediv12a  11798  ledivp1  11807  ltdiv23i  11829  ledivp1i  11830  ltdivp1i  11831  infm3  11864  8th4div3  12123  gtndiv  12327  nn0ind  12345  xrre2  12833  2resupmax  12851  qsqueeze  12864  xmulpnf1  12937  xlemul1a  12951  ioorebas  13112  elfz0ubfz0  13289  le2sq2  13782  expubnd  13823  crreczi  13871  bccl  13964  hashbc  14093  wrdred1hash  14192  ccatlid  14219  shftfval  14709  sgnp  14729  sqreulem  14999  binom1p  15471  fallrisefac  15663  efsub  15737  efi4p  15774  sinadd  15801  cosadd  15802  demoivreALT  15838  rpnnen2lem4  15854  odd2np1  15978  opoe  16000  omoe  16001  opeo  16002  omeo  16003  divalglem4  16033  divalglem9  16038  gcdcllem3  16136  gcdadd  16161  algcvgblem  16210  isprm3  16316  1arith2  16557  vdwap0  16605  vdwap1  16606  ipolt  18168  smndex1sgrp  18462  f1otrspeq  18970  rmodislmod  20106  rmodislmodOLD  20107  cnfldneg  20536  cnflddiv  20540  cnfldmulg  20542  cnfldexp  20543  zringmulg  20590  zringsubgval  20604  remulg  20724  resubgval  20726  thlleval  20815  mplsubrglem  21120  evls1rhm  21398  iccordt  22273  bl2ioo  23861  xrsblre  23880  iccntr  23890  icccmplem3  23893  reconnlem2  23896  opnreen  23900  iccpnfcnv  24013  cnllycmp  24025  pcoptcl  24090  ismbl2  24596  cmmbl  24603  nulmbl  24604  unmbl  24606  voliunlem2  24620  ioombl1  24631  opnmbllem  24670  mbfima  24699  ellimc3  24948  limcflf  24950  coe1termlem  25324  dvnply2  25352  dvnply  25353  reeff1o  25511  sinperlem  25542  resinf1o  25597  logeftb  25644  logge0  25665  efopn  25718  loglesqrt  25816  logrec  25818  xrlimcnp  26023  ppinncl  26228  chtrpcl  26229  bposlem2  26338  bposlem8  26344  lgsdir2  26383  1lgs  26393  ax5seglem2  27200  axcontlem2  27236  fusgrfis  27600  3cyclfrgrrn  28551  isgrpoi  28761  imsmetlem  28953  nmcvcn  28958  ipval2  28970  lnocoi  29020  nmlno0lem  29056  nmblolbii  29062  blometi  29066  blocnilem  29067  blocni  29068  ipasslem1  29094  ipasslem2  29095  ipasslem4  29097  ipasslem5  29098  ipasslem8  29100  ipblnfi  29118  ip2eqi  29119  ubthlem1  29133  htthlem  29180  h2hmetdval  29241  axhvcom-zf  29246  axhis1-zf  29257  axhis4-zf  29260  hvm1neg  29295  hvsub4  29300  hvsubass  29307  hvsubdistr2  29313  hv2times  29324  hvsubcan  29337  hvsubcan2  29338  his2sub  29355  norm-i  29392  normpyc  29409  hhip  29440  hhph  29441  norm1exi  29513  hhssabloilem  29524  hhssnv  29527  hhshsslem2  29531  hhssmetdval  29540  shscli  29580  shunssi  29631  shsleji  29633  shsidmi  29647  spanunsni  29842  h1datomi  29844  spansncvi  29915  pjss2i  29943  pjssmii  29944  pjocini  29961  homulid2  30063  honegdi  30072  ho2times  30082  nmopge0  30174  nmopgt0  30175  nmfnge0  30190  lnopaddi  30234  lnopmuli  30235  lnopsubi  30237  hmopbdoptHIL  30251  nmbdoplbi  30287  nmcoplbi  30291  nmophmi  30294  lnopconi  30297  lnfnaddi  30306  lnfnsubi  30309  nmbdfnlbi  30312  nmcfnlbi  30315  lnfnconi  30318  imaelshi  30321  cnlnadjlem2  30331  cnlnadjlem7  30336  nmoptrii  30357  nmopcoi  30358  adjcoi  30363  nmopcoadji  30364  bracnlnval  30377  leopmul  30397  opsqrlem1  30403  opsqrlem6  30408  hmopidmpji  30415  sto2i  30500  strlem1  30513  atcveq0  30611  atcv0eq  30642  atomli  30645  atcvati  30649  atcvat3i  30659  cdjreui  30695  cdj1i  30696  xdiv0  31105  xdivpnfrp  31109  mhmhmeotmd  31779  rezh  31821  qqhucn  31842  blsconn  33106  cnllysconn  33107  sate0fv0  33279  prv0  33292  sinccvglem  33530  ttrcltr  33702  nosupno  33833  nosupbday  33835  noinfno  33848  noinfbday  33850  noetasuplem4  33866  lrrecfr  34027  opnrebl2  34437  ptrecube  35704  poimirlem6  35710  poimirlem7  35711  poimirlem29  35733  poimirlem30  35734  opnmbllem0  35740  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  voliunnfl  35748  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  heiborlem7  35902  rrnequiv  35920  ismrer1  35923  el3v1  36299  cnaddcom  36913  lcmineqlem1  39965  2xp3dxp2ge1d  40090  sn-ltaddpos  40344  mapco2  40453  mzpaddmpt  40479  mzpmulmpt  40480  zindbi  40684  mpaaeu  40891  eel000cT  42212  eel0TT  42213  supminfxr  42894  fmtno4prmfac  44912  aacllem  46391