Theorem mp3an1 1440

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  mp3an12  1443  mp3an1i  1446  mp3anl1  1447  mp3an  1453  mp3an2i  1458  mp3an3an  1459  onint  7373  wfrlem12  7825  tfrlem9  7880  oaord1  8034  oaword2  8036  oawordeulem  8037  oa00  8042  omword1  8056  omword2  8057  omlimcl  8061  oeoelem  8081  nnaordex  8121  enp1i  8606  dffi3  8748  unbnn3  8975  pwdjuen  9460  zorn2  9781  zornn0  9783  ttukey  9793  brdom7disj  9806  brdom6disj  9807  muladd11  10663  negsubdi  10796  mulneg1  10930  ltaddpos  10984  addge01  11004  reccl  11159  recid  11166  recid2  11167  recdiv2  11207  divdiv23zi  11247  ltmul12a  11350  lemul12a  11352  mulgt1  11353  ltmulgt11  11354  gt0div  11360  ge0div  11361  lediv12a  11387  ledivp1  11396  ltdiv23i  11418  ledivp1i  11419  ltdivp1i  11420  infm3  11454  8th4div3  11711  gtndiv  11913  nn0ind  11931  xrre2  12417  2resupmax  12435  qsqueeze  12448  xmulpnf1  12521  xlemul1a  12535  ioorebas  12693  elfz0ubfz0  12865  le2sq2  13354  expubnd  13395  crreczi  13443  bccl  13536  hashbc  13663  wrdred1hash  13763  ccatlid  13788  shftfval  14267  sgnp  14287  sqreulem  14557  binom1p  15023  fallrisefac  15216  efsub  15290  efi4p  15327  sinadd  15354  cosadd  15355  demoivreALT  15391  rpnnen2lem4  15407  odd2np1  15527  opoe  15549  omoe  15550  opeo  15551  omeo  15552  divalglem4  15584  divalglem9  15589  gcdcllem3  15687  gcdadd  15711  algcvgblem  15754  isprm3  15860  1arith2  16097  vdwap0  16145  vdwap1  16146  ipolt  17602  f1otrspeq  18310  rmodislmod  19396  mplsubrglem  19911  evls1rhm  20172  cnfldneg  20257  cnflddiv  20261  cnfldmulg  20263  cnfldexp  20264  zringmulg  20311  remulg  20437  resubgval  20439  thlleval  20528  frlmsslsp  20626  iccordt  21510  bl2ioo  23087  xrsblre  23106  iccntr  23116  icccmplem3  23119  reconnlem2  23122  opnreen  23126  iccpnfcnv  23235  cnllycmp  23247  pcoptcl  23312  ismbl2  23815  cmmbl  23822  nulmbl  23823  unmbl  23825  voliunlem2  23839  ioombl1  23850  opnmbllem  23889  mbfima  23918  ellimc3  24164  limcflf  24166  coe1termlem  24535  dvnply2  24563  dvnply  24564  reeff1o  24722  sinperlem  24753  resinf1o  24805  logeftb  24852  logge0  24873  efopn  24926  loglesqrt  25024  logrec  25026  xrlimcnp  25232  ppinncl  25437  chtrpcl  25438  bposlem2  25547  bposlem8  25553  lgsdir2  25592  1lgs  25602  ax5seglem2  26402  axcontlem2  26438  fusgrfis  26799  3cyclfrgrrn  27753  isgrpoi  27962  imsmetlem  28154  nmcvcn  28159  ipval2  28171  lnocoi  28221  nmlno0lem  28257  nmblolbii  28263  blometi  28267  blocnilem  28268  blocni  28269  ipasslem1  28295  ipasslem2  28296  ipasslem4  28298  ipasslem5  28299  ipasslem8  28301  ipblnfi  28319  ip2eqi  28320  ubthlem1  28334  htthlem  28381  h2hmetdval  28442  axhvcom-zf  28447  axhis1-zf  28458  axhis4-zf  28461  hvm1neg  28496  hvsub4  28501  hvsubass  28508  hvsubdistr2  28514  hv2times  28525  hvsubcan  28538  hvsubcan2  28539  his2sub  28556  norm-i  28593  normpyc  28610  hhip  28641  hhph  28642  norm1exi  28714  hhssabloilem  28725  hhssnv  28728  hhshsslem2  28732  hhssmetdval  28741  shscli  28781  shunssi  28832  shsleji  28834  shsidmi  28848  spanunsni  29043  h1datomi  29045  spansncvi  29116  pjss2i  29144  pjssmii  29145  pjocini  29162  homulid2  29264  honegdi  29273  ho2times  29283  nmopge0  29375  nmopgt0  29376  nmfnge0  29391  lnopaddi  29435  lnopmuli  29436  lnopsubi  29438  hmopbdoptHIL  29452  nmbdoplbi  29488  nmcoplbi  29492  nmophmi  29495  lnopconi  29498  lnfnaddi  29507  lnfnsubi  29510  nmbdfnlbi  29513  nmcfnlbi  29516  lnfnconi  29519  imaelshi  29522  cnlnadjlem2  29532  cnlnadjlem7  29537  nmoptrii  29558  nmopcoi  29559  adjcoi  29564  nmopcoadji  29565  bracnlnval  29578  leopmul  29598  opsqrlem1  29604  opsqrlem6  29609  hmopidmpji  29616  sto2i  29701  strlem1  29714  atcveq0  29812  atcv0eq  29843  atomli  29846  atcvati  29850  atcvat3i  29860  cdjreui  29896  cdj1i  29897  xdiv0  30285  xdivpnfrp  30289  mhmhmeotmd  30783  rezh  30825  qqhucn  30846  blsconn  32101  cnllysconn  32102  sate0fv0  32274  prv0  32287  sinccvglem  32525  nosupno  32814  nosupbday  32816  noetalem3  32830  opnrebl2  33280  ptrecube  34444  poimirlem6  34450  poimirlem7  34451  poimirlem29  34473  poimirlem30  34474  opnmbllem0  34480  mblfinlem3  34483  mblfinlem4  34484  ismblfin  34485  voliunnfl  34488  ftc1anclem5  34523  ftc1anclem7  34525  ftc1anclem8  34526  ftc1anc  34527  heiborlem7  34648  rrnequiv  34666  ismrer1  34669  el3v1  35045  cnaddcom  35660  mapco2  38818  mzpaddmpt  38844  mzpmulmpt  38845  zindbi  39049  mpaaeu  39256  eel000cT  40597  eel0TT  40598  supminfxr  41303  fmtno4prmfac  43238  zringsubgval  43951  aacllem  44404