Theorem mp3an1 1256

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  mp3an12  1259  mp3an1i  1262  mp3anl1  1263  mp3an  1269  mp3an2i  1274  mp3an3an  1275  tfrlem9  5968  rdgexgg  6027  oaexg  6092  omexg  6095  oeiexg  6097  oav2  6107  nnaordex  6166  mulidnq  6641  1idpru  6843  addgt0sr  7014  muladd11  7308  cnegex  7353  negsubdi  7431  renegcl  7436  mulneg1  7566  ltaddpos  7623  addge01  7643  rimul  7752  recclap  7834  recidap  7841  recidap2  7842  recdivap2  7880  divdiv23apzi  7920  ltmul12a  8005  lemul12a  8007  mulgt1  8008  ltmulgt11  8009  gt0div  8015  ge0div  8016  ltdiv23i  8071  8th4div3  8317  gtndiv  8523  nn0ind  8542  fnn0ind  8544  xrre2  8964  ioorebasg  9074  fzen  9138  elfz0ubfz0  9213  expubnd  9630  le2sq2  9648  bernneq  9690  expnbnd  9693  faclbnd6  9768  bccl  9791  shftfval  9847  mulreap  9889  caucvgrelemrec  10003  odd2np1  10417  opoe  10439  omoe  10440  opeo  10441  omeo  10442  gcdadd  10520  gcdmultiple  10553  algcvgblem  10575  ialgcvga  10577  isprm3  10644  coprm  10667