Theorem mpancom 422

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpancom.1	⊢ (𝜓 → 𝜑)
mpancom.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpancom	⊢ (𝜓 → 𝜒)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 ⊢ (𝜓 → 𝜑)
2		id 19	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpan  424  spesbc  3048  onsucelsucr  4507  sucunielr  4509  ordsuc  4562  peano2b  4614  xpiindim  4764  fvelrnb  5563  fliftcnv  5795  riotaprop  5853  unielxp  6174  dmtpos  6256  tpossym  6276  ercnv  6555  cnvct  6808  php5dom  6862  3xpfi  6929  recrecnq  7392  1idpr  7590  eqlei2  8051  lem1  8803  eluzfz1  10030  fzpred  10069  uznfz  10102  fz0fzdiffz0  10129  fzctr  10132  flid  10283  flqeqceilz  10317  faclbnd3  10722  bcn1  10737  isfinite4im  10771  leabs  11082  gcd0id  11979  lcmgcdlem  12076  dvdsnprmd  12124  pcprod  12343  fldivp1  12345  intopsn  12785  mgm1  12788  sgrp1  12815  mnd1  12846  mnd1id  12847  grp1  12975  grp1inv  12976  eqger  13081  eqgid  13083  ring1  13234  ringressid  13236  subrgsubm  13353  cncrng  13433  eltpsg  13510  tg1  13529  cldval  13569  cldss  13575  cldopn  13577  psmetdmdm  13794  dvef  14158  relogef  14255  zabsle1  14370  bj-nn0suc0  14672