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  6590  rdgexgg  6649  oaexg  6721  omexg  6724  oeiexg  6726  oav2  6736  nnaordex  6801  mulidnq  7757  1idpru  7959  addgt0sr  8143  muladd11  8461  cnegex  8506  negsubdi  8584  renegcl  8589  mulneg1  8724  ltaddpos  8782  addge01  8802  rimul  8916  recclap  9012  recidap  9019  recidap2  9020  recdivap2  9058  divdiv23apzi  9098  ltmul12a  9193  lemul12a  9195  mulgt1  9196  ltmulgt11  9197  gt0div  9203  ge0div  9204  ltdiv23i  9259  8th4div3  9529  gtndiv  9746  nn0ind  9765  fnn0ind  9767  xrre2  10234  ioorebasg  10388  fzen  10458  elfz0ubfz0  10543  expubnd  11048  le2sq2  11067  bernneq  11113  expnbnd  11116  faclbnd6  11198  bccl  11221  hashfibc  11299  hashfacen  11300  wrdred1hash  11364  ccatlid  11390  swrd0g  11448  shftfval  11602  mulreap  11645  caucvgrelemrec  11761  binom1p  12271  efi4p  12503  sinadd  12522  cosadd  12523  cos2t  12536  cos2tsin  12537  absefib  12557  efieq1re  12558  demoivreALT  12560  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  gcdadd  12781  gcdmultiple  12816  algcvgblem  12846  algcvga  12848  isprm3  12915  coprm  12942  1arith2  13170  ballotfilem2  13280  rmodislmod  14772  cnfldneg  14994  cnfldmulg  14997  cnfldexp  14998  zringmulg  15017  zringsubgval  15024  bl2ioo  15742  ioo2blex  15744  mpomulcn  15758  sinperlem  16001  logge0  16074  ppiqnncl  16239  chtqrpcl  16240  bposlem2  16273  bposlem8  16279  lgsdir2  16318  1lgs  16328