Theorem mp3an1 1337

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

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

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 983

This theorem is referenced by:  mp3an12  1340  mp3an1i  1343  mp3anl1  1344  mp3an  1350  mp3an2i  1355  mp3an3an  1356  tfrlem9  6407  rdgexgg  6466  oaexg  6536  omexg  6539  oeiexg  6541  oav2  6551  nnaordex  6616  mulidnq  7504  1idpru  7706  addgt0sr  7890  muladd11  8207  cnegex  8252  negsubdi  8330  renegcl  8335  mulneg1  8469  ltaddpos  8527  addge01  8547  rimul  8660  recclap  8754  recidap  8761  recidap2  8762  recdivap2  8800  divdiv23apzi  8840  ltmul12a  8935  lemul12a  8937  mulgt1  8938  ltmulgt11  8939  gt0div  8945  ge0div  8946  ltdiv23i  9001  8th4div3  9258  gtndiv  9470  nn0ind  9489  fnn0ind  9491  xrre2  9945  ioorebasg  10099  fzen  10167  elfz0ubfz0  10249  expubnd  10743  le2sq2  10762  bernneq  10807  expnbnd  10810  faclbnd6  10891  bccl  10914  hashfacen  10983  wrdred1hash  11039  ccatlid  11065  swrd0g  11116  shftfval  11165  mulreap  11208  caucvgrelemrec  11323  binom1p  11829  efi4p  12061  sinadd  12080  cosadd  12081  cos2t  12094  cos2tsin  12095  absefib  12115  efieq1re  12116  demoivreALT  12118  odd2np1  12217  opoe  12239  omoe  12240  opeo  12241  omeo  12242  gcdadd  12339  gcdmultiple  12374  algcvgblem  12404  algcvga  12406  isprm3  12473  coprm  12499  1arith2  12724  rmodislmod  14146  cnfldneg  14368  cnfldmulg  14371  cnfldexp  14372  zringmulg  14393  zringsubgval  14400  bl2ioo  15055  ioo2blex  15057  mpomulcn  15071  sinperlem  15313  logge0  15385  lgsdir2  15543  1lgs  15553