Theorem mp3an1 1365

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an12  1368  mp3an1i  1371  mp3anl1  1372  mp3an  1378  mp3an2i  1383  mp3an3an  1384  tfrlem9  6594  rdgexgg  6653  oaexg  6725  omexg  6728  oeiexg  6730  oav2  6740  nnaordex  6805  mulidnq  7762  1idpru  7964  addgt0sr  8148  muladd11  8466  cnegex  8511  negsubdi  8589  renegcl  8594  mulneg1  8729  ltaddpos  8787  addge01  8807  rimul  8921  recclap  9017  recidap  9024  recidap2  9025  recdivap2  9063  divdiv23apzi  9103  ltmul12a  9198  lemul12a  9200  mulgt1  9201  ltmulgt11  9202  gt0div  9208  ge0div  9209  ltdiv23i  9264  8th4div3  9535  gtndiv  9752  nn0ind  9771  fnn0ind  9773  xrre2  10240  ioorebasg  10394  fzen  10464  elfz0ubfz0  10549  expubnd  11054  le2sq2  11073  bernneq  11119  expnbnd  11122  faclbnd6  11204  bccl  11227  hashfibc  11305  hashfacen  11306  wrdred1hash  11370  ccatlid  11396  swrd0g  11454  shftfval  11608  mulreap  11651  caucvgrelemrec  11767  binom1p  12277  efi4p  12509  sinadd  12528  cosadd  12529  cos2t  12542  cos2tsin  12543  absefib  12563  efieq1re  12564  demoivreALT  12566  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  gcdadd  12787  gcdmultiple  12822  algcvgblem  12852  algcvga  12854  isprm3  12921  coprm  12948  1arith2  13176  ballotfilem2  13286  rmodislmod  14797  cnfldneg  15019  cnfldmulg  15022  cnfldexp  15023  zringmulg  15042  zringsubgval  15049  bl2ioo  15776  ioo2blex  15778  mpomulcn  15792  sinperlem  16035  logge0  16110  ppiqnncl  16278  chtqrpcl  16279  bposlem2  16312  bposlem8  16318  lgsdir2  16357  1lgs  16367