Theorem impcom 125

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
impcom	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 30	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mpan9  281  19.41h  1707  19.41  1708  equtr2  1733  mopick  2131  2euex  2140  gencl  2803  2gencl  2804  rspccva  2875  indifdir  3428  sseq0  3501  minel  3521  r19.2m  3546  r19.2mOLD  3547  elelpwi  3627  ssuni  3871  disjiun  4038  trintssm  4157  ssexg  4182  pofun  4357  sowlin  4365  2optocl  4750  3optocl  4751  elrnmpt1  4927  resieq  4966  fnun  5376  fss  5431  fun  5442  dmfex  5459  fvelimab  5629  mptfvex  5659  fmptco  5740  fnressn  5760  fressnfv  5761  fvtp2g  5783  fvtp3g  5784  fnex  5796  funfvima3  5808  isores3  5874  f1o2ndf1  6304  reldmtpos  6329  smores  6368  tfrlem7  6393  tfrlemi1  6408  tfrexlem  6410  tfrcl  6440  frecrdg  6484  nnacl  6556  nnmcl  6557  nnmsucr  6564  nntri3or  6569  nnaword  6587  nnaordex  6604  2ecoptocl  6700  ssct  6895  enm  6897  xpf1o  6923  ac6sfi  6977  f1dmvrnfibi  7028  f1vrnfibi  7029  updjud  7166  enumct  7199  nnnninfeq  7212  exmidontriimlem4  7318  exmidontriim  7319  elni2  7409  ax1rid  7972  negf1o  8436  mulgt1  8918  lbreu  9000  nnaddcl  9038  nnmulcl  9039  zaddcllempos  9391  zaddcllemneg  9393  nn0n0n1ge2b  9434  fzind  9470  fnn0ind  9471  uzaddcl  9689  elpq  9752  uzsubsubfz  10151  elfz1b  10194  elfz0ubfz0  10229  fz0fzdiffz0  10234  elfzmlbp  10236  fzofzim  10293  elfzom1elp1fzo  10312  elfzom1p1elfzo  10324  ssfzo12bi  10335  modfzo0difsn  10521  seq3val  10586  seqvalcd  10587  expcllem  10676  expap0  10695  apexp1  10844  faclbnd  10867  faclbnd6  10870  fihashf1rn  10914  omgadd  10928  hashfzp1  10950  seq3coll  10968  lswlgt0cl  11020  ccatsymb  11033  cjexp  11123  r19.29uz  11222  resqrexlemover  11240  resqrexlemlo  11243  resqrexlemcalc3  11246  absexp  11309  fimaxre2  11457  climshft  11534  climub  11574  climserle  11575  sumfct  11604  isumss2  11623  binom  11714  bcxmas  11719  clim2prod  11769  prodfap0  11775  prodfrecap  11776  prodfct  11817  demoivreALT  12004  dvdsdivcl  12080  dvdsfac  12090  oddnn02np1  12110  oddge22np1  12111  evennn02n  12112  evennn2n  12113  m1exp1  12131  nn0o  12137  flodddiv4  12166  gcdneg  12222  bezoutlemmain  12238  dfgcd2  12254  gcdmultiple  12260  nnwosdc  12279  alginv  12288  cncongr1  12344  prmdvdsexp  12389  prmndvdsfaclt  12397  dfgrp2  13277  srgmulgass  13669  lmodvsmmulgdi  14003  lmodfopnelem1  14004  rmodislmodlem  14030  cnfldmulg  14256  cnfldexp  14257  clsss  14508  xmettri2  14751  mettri  14763  metss  14884  plycolemc  15148  zabsle1  15394  gausslemma2dlem1a  15453  gausslemma2dlem2  15457  gausslemma2dlem3  15458  gausslemma2dlem4  15459  2lgslem1a1  15481  bdssexg  15704  bj-findis  15779  nninfalllem1  15809  nninfsellemdc  15811  redc0  15860