Theorem mp3an1 1230

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

Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 896

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

This theorem depends on definitions:  df-bi 114  df-3an 898

This theorem is referenced by:  mp3an12  1233  mp3an1i  1236  mp3anl1  1237  mp3an  1243  mp3an2i  1248  mp3an3an  1249  tfrlem9  5965  rdgexgg  5995  oaexg  6058  omexg  6061  oeiexg  6063  oav2  6073  nnaordex  6130  mulidnq  6544  1idpru  6746  addgt0sr  6917  muladd11  7206  cnegex  7251  negsubdi  7329  renegcl  7334  mulneg1  7463  ltaddpos  7520  addge01  7540  rimul  7649  recclap  7731  recidap  7738  recidap2  7739  recdivap2  7775  divdiv23apzi  7815  ltmul12a  7900  lemul12a  7902  mulgt1  7903  ltmulgt11  7904  gt0div  7910  ge0div  7911  ltdiv23i  7966  8th4div3  8200  gtndiv  8392  nn0ind  8410  fnn0ind  8412  xrre2  8834  ioorebasg  8944  fzen  9008  elfz0ubfz0  9083  frec2uzzd  9344  frec2uzsucd  9345  expubnd  9471  le2sq2  9489  bernneq  9530  expnbnd  9533  faclbnd6  9605  bccl  9628  shftfval  9643  mulreap  9685  caucvgrelemrec  9799  odd2np1  10176  opoe  10199  omoe  10200  opeo  10201  omeo  10202  algcvgblem  10243  ialgcvga  10245