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  6348  rdgexgg  6407  oaexg  6477  omexg  6480  oeiexg  6482  oav2  6492  nnaordex  6557  mulidnq  7423  1idpru  7625  addgt0sr  7809  muladd11  8125  cnegex  8170  negsubdi  8248  renegcl  8253  mulneg1  8387  ltaddpos  8444  addge01  8464  rimul  8577  recclap  8671  recidap  8678  recidap2  8679  recdivap2  8717  divdiv23apzi  8757  ltmul12a  8852  lemul12a  8854  mulgt1  8855  ltmulgt11  8856  gt0div  8862  ge0div  8863  ltdiv23i  8918  8th4div3  9173  gtndiv  9383  nn0ind  9402  fnn0ind  9404  xrre2  9857  ioorebasg  10011  fzen  10079  elfz0ubfz0  10161  expubnd  10617  le2sq2  10636  bernneq  10681  expnbnd  10684  faclbnd6  10765  bccl  10788  hashfacen  10857  shftfval  10871  mulreap  10914  caucvgrelemrec  11029  binom1p  11534  efi4p  11766  sinadd  11785  cosadd  11786  cos2t  11799  cos2tsin  11800  absefib  11819  efieq1re  11820  demoivreALT  11822  odd2np1  11919  opoe  11941  omoe  11942  opeo  11943  omeo  11944  gcdadd  12027  gcdmultiple  12062  algcvgblem  12092  algcvga  12094  isprm3  12161  coprm  12187  1arith2  12411  rmodislmod  13692  cnfldneg  13901  cnfldmulg  13904  cnfldexp  13905  zringmulg  13922  zringsubgval  13929  bl2ioo  14527  ioo2blex  14529  sinperlem  14714  logge0  14786  lgsdir2  14920  1lgs  14930