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  3119  onsucelsucr  4612  sucunielr  4614  ordsuc  4667  peano2b  4719  xpiindim  4873  fununfun  5380  fvelrnb  5702  fliftcnv  5946  riotaprop  6007  unielxp  6346  dmtpos  6465  tpossym  6485  ercnv  6766  cnvct  7027  php5dom  7092  3xpfi  7169  recrecnq  7657  1idpr  7855  eqlei2  8317  lem1  9070  eluzfz1  10309  fzpred  10348  uznfz  10381  fz0fzdiffz0  10408  fzctr  10411  flid  10588  flqeqceilz  10624  faclbnd3  11049  bcn1  11064  isfinite4im  11098  leabs  11695  gcd0id  12611  lcmgcdlem  12710  dvdsnprmd  12758  pcprod  12980  fldivp1  12982  intopsn  13511  mgm1  13514  sgrp1  13555  mnd1  13599  mnd1id  13600  grp1  13750  grp1inv  13751  eqger  13872  eqgid  13874  qusghm  13930  rngressid  14029  ring1  14134  ringressid  14138  subrgsubm  14310  resrhm2b  14325  lssex  14430  cncrng  14645  psrbaglesupp  14749  eltpsg  14831  tg1  14850  cldval  14890  cldss  14896  cldopn  14898  psmetdmdm  15115  dvef  15518  relogef  15655  zabsle1  15798  usgredg2vlem2  16144  wlkprop  16248  wlkvtxiedg  16266  eupthseg  16373  bj-nn0suc0  16646