Theorem mp3an1 1335

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  mp3an12  1338  mp3an1i  1341  mp3anl1  1342  mp3an  1348  mp3an2i  1353  mp3an3an  1354  tfrlem9  6374  rdgexgg  6433  oaexg  6503  omexg  6506  oeiexg  6508  oav2  6518  nnaordex  6583  mulidnq  7451  1idpru  7653  addgt0sr  7837  muladd11  8154  cnegex  8199  negsubdi  8277  renegcl  8282  mulneg1  8416  ltaddpos  8473  addge01  8493  rimul  8606  recclap  8700  recidap  8707  recidap2  8708  recdivap2  8746  divdiv23apzi  8786  ltmul12a  8881  lemul12a  8883  mulgt1  8884  ltmulgt11  8885  gt0div  8891  ge0div  8892  ltdiv23i  8947  8th4div3  9204  gtndiv  9415  nn0ind  9434  fnn0ind  9436  xrre2  9890  ioorebasg  10044  fzen  10112  elfz0ubfz0  10194  expubnd  10670  le2sq2  10689  bernneq  10734  expnbnd  10737  faclbnd6  10818  bccl  10841  hashfacen  10910  wrdred1hash  10960  shftfval  10968  mulreap  11011  caucvgrelemrec  11126  binom1p  11631  efi4p  11863  sinadd  11882  cosadd  11883  cos2t  11896  cos2tsin  11897  absefib  11917  efieq1re  11918  demoivreALT  11920  odd2np1  12017  opoe  12039  omoe  12040  opeo  12041  omeo  12042  gcdadd  12125  gcdmultiple  12160  algcvgblem  12190  algcvga  12192  isprm3  12259  coprm  12285  1arith2  12509  rmodislmod  13850  cnfldneg  14072  cnfldmulg  14075  cnfldexp  14076  zringmulg  14097  zringsubgval  14104  bl2ioo  14729  ioo2blex  14731  mpomulcn  14745  sinperlem  14984  logge0  15056  lgsdir2  15190  1lgs  15200