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 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

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

This theorem is used by:  mpan9  281  19.41h  1737  19.41  1738  equtr2  1763  mopick  2165  2euex  2174  gencl  2854  2gencl  2855  vtocl4g  2894  vtocl4ga  2895  rspccva  2928  indifdir  3487  minel  3586  r19.2m  3614  r19.2mOLD  3615  elelpwi  3701  ssuni  3957  disjiun  4125  trintssm  4247  ssexg  4274  pofun  4459  sowlin  4467  2optocl  4854  3optocl  4855  ssrelrn  4974  elrnmpt1  5035  resieq  5075  fnun  5492  fss  5549  fun  5564  dmfex  5585  fvelimab  5762  mptfvex  5794  fmptco  5877  fnressn  5904  fressnfv  5905  fvtp2g  5927  fvtp3g  5928  fnex  5940  funfvima3  5955  isores3  6024  f1o2ndf1  6468  funsssuppss  6502  reldmtpos  6529  smores  6568  tfrlem7  6593  tfrlemi1  6608  tfrexlem  6610  tfrcl  6640  frecrdg  6684  nnacl  6758  nnmcl  6759  nnmsucr  6766  nntri3or  6771  nnaword  6789  nnaordex  6806  2ecoptocl  6902  ssct  7120  enm  7124  xpf1o  7150  ac6sfi  7208  f1dmvrnfibi  7264  f1vrnfibi  7265  updjud  7428  enumct  7461  nnnninfeq  7474  exmidontriimlem4  7586  exmidontriim  7587  elni2  7687  ax1rid  8250  negf1o  8716  mulgt1  9201  lbreu  9283  nnaddcl  9333  nnmulcl  9334  zaddcllempos  9690  zaddcllemneg  9692  nn0n0n1ge2b  9734  fzind  9771  fnn0ind  9772  uzaddcl  10001  elpq  10065  uzsubsubfz  10468  elfz1b  10513  elfz0ubfz0  10548  fz0fzdiffz0  10553  elfzmlbp  10555  fzofzim  10616  elfzom1elp1fzo  10636  elfzom1p1elfzo  10648  ssfzo12bi  10659  modfzo0difsn  10852  seq3val  10917  seqvalcd  10918  expcllem  11007  expap0  11026  apexp1  11177  faclbnd  11200  faclbnd6  11203  fihashf1rn  11248  omgadd  11263  hashfzp1  11286  hashmap  11289  seq3coll  11315  fundm2domnop0  11321  lswlgt0cl  11378  ccatsymb  11391  swrdnd  11452  swrd0g  11453  swrdspsleq  11460  pfxsuff1eqwrdeq  11492  swrdswrdlem  11497  swrdswrd  11498  wrd2ind  11516  pfxccatin12lem2a  11520  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  pfxccat3a  11531  swrdccat3blem  11532  cjexp  11679  r19.29uz  11779  resqrexlemover  11797  resqrexlemlo  11800  resqrexlemcalc3  11803  absexp  11867  fimaxre2  12015  climshft  12094  climub  12134  climserle  12135  sumfct  12164  isumss2  12184  binom  12275  bcxmas  12280  clim2prod  12330  prodfap0  12336  prodfrecap  12337  prodfct  12378  demoivreALT  12565  dvdsdivcl  12641  dvdsfac  12651  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  m1exp1  12692  nn0o  12698  flodddiv4  12727  gcdneg  12783  bezoutlemmain  12799  dfgcd2  12815  gcdmultiple  12821  nnwosdc  12840  alginv  12849  cncongr1  12905  prmdvdsexp  12951  prmndvdsfaclt  12959  dfgrp2  13890  srgmulgass  14399  lmodvsmmulgdi  14768  lmodfopnelem1  14769  rmodislmodlem  14795  cnfldmulg  15021  cnfldexp  15022  assamulgscm  15151  clsss  15361  xmettri2  15604  mettri  15616  metss  15737  plycolemc  16001  zabsle1  16340  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem3  16404  gausslemma2dlem4  16405  2lgslem1a1  16427  incistruhgr  16553  umgrislfupgrenlem  16593  uhgr2edg  16669  usgredg2vlem2  16686  subgrfun  16730  wlkl1loop  16821  wlkres  16842  clwwlkccatlem  16863  isclwwlknx  16879  clwwlkext2edg  16885  clwwlknonel  16895  clwwlknonex2lem2  16901  clwwlknun  16904  depindlem2  16970  depindlem3  16971  bdssexg  17152  bj-findis  17227  nninfalllem1  17274  nninfsellemdc  17276  redc0  17331