Theorem mpanl12 440

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mpanl12.1	⊢ 𝜑
mpanl12.2	⊢ 𝜓
mpanl12.3	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpanl12	⊢ (𝜒 → 𝜃)

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 ⊢ 𝜓
2		mpanl12.1	. . 3 ⊢ 𝜑
3		mpanl12.3	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpanl1 438	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 428	1 ⊢ (𝜒 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reuun1  3515  ordtri2orexmid  4672  opthreg  4705  ordtri2or2exmid  4720  ontri2orexmidim  4721  fvtp1  5929  nq0m0r  7830  nq02m  7839  gt0srpr  8122  map2psrprg  8179  pitoregt0  8223  axcnre  8255  addgt0  8784  addgegt0  8785  addgtge0  8786  addge0  8787  addgt0i  8824  addge0i  8825  addgegt0i  8826  add20i  8828  mulge0i  8957  recextlem1  8988  recap0  9024  recdivap  9057  recgt1  9236  prodgt0i  9247  prodge0i  9248  iccshftri  10415  iccshftli  10417  iccdili  10419  icccntri  10421  mulexpzap  11038  expaddzap  11042  m1expeven  11045  iexpcyc  11103  amgm2  11908  ege2le3  12464  sqnprm  12941  prmlem1  13252  prmlem2  13264  lmres  15486  2logb9irrap  16225  bposlem7  16329