Theorem mp3an1 1444

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mp3an12  1447  mp3an1i  1450  mp3anl1  1451  mp3an  1457  mp3an2i  1462  mp3an3an  1463  onint  7504  wfrlem12  7960  tfrlem9  8015  oaord1  8171  oaword2  8173  oawordeulem  8174  oa00  8179  omword1  8193  omword2  8194  omlimcl  8198  oeoelem  8218  nnaordex  8258  enp1i  8747  dffi3  8889  unbnn3  9116  pwdjuen  9601  zorn2  9922  zornn0  9924  ttukey  9934  brdom7disj  9947  brdom6disj  9948  muladd11  10804  negsubdi  10936  mulneg1  11070  ltaddpos  11124  addge01  11144  reccl  11299  recid  11306  recid2  11307  recdiv2  11347  divdiv23zi  11387  ltmul12a  11490  lemul12a  11492  mulgt1  11493  ltmulgt11  11494  gt0div  11500  ge0div  11501  lediv12a  11527  ledivp1  11536  ltdiv23i  11558  ledivp1i  11559  ltdivp1i  11560  infm3  11594  8th4div3  11851  gtndiv  12053  nn0ind  12071  xrre2  12557  2resupmax  12575  qsqueeze  12588  xmulpnf1  12661  xlemul1a  12675  ioorebas  12833  elfz0ubfz0  13005  le2sq2  13494  expubnd  13535  crreczi  13583  bccl  13676  hashbc  13805  wrdred1hash  13907  ccatlid  13934  shftfval  14423  sgnp  14443  sqreulem  14713  binom1p  15180  fallrisefac  15373  efsub  15447  efi4p  15484  sinadd  15511  cosadd  15512  demoivreALT  15548  rpnnen2lem4  15564  odd2np1  15684  opoe  15706  omoe  15707  opeo  15708  omeo  15709  divalglem4  15741  divalglem9  15746  gcdcllem3  15844  gcdadd  15868  algcvgblem  15915  isprm3  16021  1arith2  16258  vdwap0  16306  vdwap1  16307  ipolt  17763  smndex1sgrp  18067  f1otrspeq  18569  rmodislmod  19696  mplsubrglem  20213  evls1rhm  20479  cnfldneg  20565  cnflddiv  20569  cnfldmulg  20571  cnfldexp  20572  zringmulg  20619  remulg  20745  resubgval  20747  thlleval  20836  frlmsslsp  20934  iccordt  21816  bl2ioo  23394  xrsblre  23413  iccntr  23423  icccmplem3  23426  reconnlem2  23429  opnreen  23433  iccpnfcnv  23542  cnllycmp  23554  pcoptcl  23619  ismbl2  24122  cmmbl  24129  nulmbl  24130  unmbl  24132  voliunlem2  24146  ioombl1  24157  opnmbllem  24196  mbfima  24225  ellimc3  24471  limcflf  24473  coe1termlem  24842  dvnply2  24870  dvnply  24871  reeff1o  25029  sinperlem  25060  resinf1o  25114  logeftb  25161  logge0  25182  efopn  25235  loglesqrt  25333  logrec  25335  xrlimcnp  25540  ppinncl  25745  chtrpcl  25746  bposlem2  25855  bposlem8  25861  lgsdir2  25900  1lgs  25910  ax5seglem2  26709  axcontlem2  26745  fusgrfis  27106  3cyclfrgrrn  28059  isgrpoi  28269  imsmetlem  28461  nmcvcn  28466  ipval2  28478  lnocoi  28528  nmlno0lem  28564  nmblolbii  28570  blometi  28574  blocnilem  28575  blocni  28576  ipasslem1  28602  ipasslem2  28603  ipasslem4  28605  ipasslem5  28606  ipasslem8  28608  ipblnfi  28626  ip2eqi  28627  ubthlem1  28641  htthlem  28688  h2hmetdval  28749  axhvcom-zf  28754  axhis1-zf  28765  axhis4-zf  28768  hvm1neg  28803  hvsub4  28808  hvsubass  28815  hvsubdistr2  28821  hv2times  28832  hvsubcan  28845  hvsubcan2  28846  his2sub  28863  norm-i  28900  normpyc  28917  hhip  28948  hhph  28949  norm1exi  29021  hhssabloilem  29032  hhssnv  29035  hhshsslem2  29039  hhssmetdval  29048  shscli  29088  shunssi  29139  shsleji  29141  shsidmi  29155  spanunsni  29350  h1datomi  29352  spansncvi  29423  pjss2i  29451  pjssmii  29452  pjocini  29469  homulid2  29571  honegdi  29580  ho2times  29590  nmopge0  29682  nmopgt0  29683  nmfnge0  29698  lnopaddi  29742  lnopmuli  29743  lnopsubi  29745  hmopbdoptHIL  29759  nmbdoplbi  29795  nmcoplbi  29799  nmophmi  29802  lnopconi  29805  lnfnaddi  29814  lnfnsubi  29817  nmbdfnlbi  29820  nmcfnlbi  29823  lnfnconi  29826  imaelshi  29829  cnlnadjlem2  29839  cnlnadjlem7  29844  nmoptrii  29865  nmopcoi  29866  adjcoi  29871  nmopcoadji  29872  bracnlnval  29885  leopmul  29905  opsqrlem1  29911  opsqrlem6  29916  hmopidmpji  29923  sto2i  30008  strlem1  30021  atcveq0  30119  atcv0eq  30150  atomli  30153  atcvati  30157  atcvat3i  30167  cdjreui  30203  cdj1i  30204  xdiv0  30600  xdivpnfrp  30604  mhmhmeotmd  31165  rezh  31207  qqhucn  31228  blsconn  32486  cnllysconn  32487  sate0fv0  32659  prv0  32672  sinccvglem  32910  nosupno  33198  nosupbday  33200  noetalem3  33214  opnrebl2  33664  ptrecube  34886  poimirlem6  34892  poimirlem7  34893  poimirlem29  34915  poimirlem30  34916  opnmbllem0  34922  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  voliunnfl  34930  ftc1anclem5  34965  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  heiborlem7  35089  rrnequiv  35107  ismrer1  35110  el3v1  35486  cnaddcom  36102  sn-ltaddpos  39236  mapco2  39305  mzpaddmpt  39331  mzpmulmpt  39332  zindbi  39536  mpaaeu  39743  eel000cT  41030  eel0TT  41031  supminfxr  41733  fmtno4prmfac  43728  zringsubgval  44443  aacllem  44896