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  1696  19.41  1697  equtr2  1722  mopick  2120  2euex  2129  gencl  2792  2gencl  2793  rspccva  2863  indifdir  3415  sseq0  3488  minel  3508  r19.2m  3533  r19.2mOLD  3534  elelpwi  3613  ssuni  3857  disjiun  4024  trintssm  4143  ssexg  4168  pofun  4343  sowlin  4351  2optocl  4736  3optocl  4737  elrnmpt1  4913  resieq  4952  fnun  5360  fss  5415  fun  5426  dmfex  5443  fvelimab  5613  mptfvex  5643  fmptco  5724  fnressn  5744  fressnfv  5745  fvtp2g  5767  fvtp3g  5768  fnex  5780  funfvima3  5792  isores3  5858  f1o2ndf1  6281  reldmtpos  6306  smores  6345  tfrlem7  6370  tfrlemi1  6385  tfrexlem  6387  tfrcl  6417  frecrdg  6461  nnacl  6533  nnmcl  6534  nnmsucr  6541  nntri3or  6546  nnaword  6564  nnaordex  6581  2ecoptocl  6677  ssct  6872  enm  6874  xpf1o  6900  ac6sfi  6954  f1dmvrnfibi  7003  f1vrnfibi  7004  updjud  7141  enumct  7174  nnnninfeq  7187  exmidontriimlem4  7284  exmidontriim  7285  elni2  7374  ax1rid  7937  negf1o  8401  mulgt1  8882  lbreu  8964  nnaddcl  9002  nnmulcl  9003  zaddcllempos  9354  zaddcllemneg  9356  nn0n0n1ge2b  9396  fzind  9432  fnn0ind  9433  uzaddcl  9651  elpq  9714  uzsubsubfz  10113  elfz1b  10156  elfz0ubfz0  10191  fz0fzdiffz0  10196  elfzmlbp  10198  fzofzim  10255  elfzom1elp1fzo  10269  elfzom1p1elfzo  10281  ssfzo12bi  10292  modfzo0difsn  10466  seq3val  10531  seqvalcd  10532  expcllem  10621  expap0  10640  apexp1  10789  faclbnd  10812  faclbnd6  10815  fihashf1rn  10859  omgadd  10873  hashfzp1  10895  seq3coll  10913  cjexp  11037  r19.29uz  11136  resqrexlemover  11154  resqrexlemlo  11157  resqrexlemcalc3  11160  absexp  11223  fimaxre2  11370  climshft  11447  climub  11487  climserle  11488  sumfct  11517  isumss2  11536  binom  11627  bcxmas  11632  clim2prod  11682  prodfap0  11688  prodfrecap  11689  prodfct  11730  demoivreALT  11917  dvdsdivcl  11992  dvdsfac  12002  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  m1exp1  12042  nn0o  12048  flodddiv4  12075  gcdneg  12119  bezoutlemmain  12135  dfgcd2  12151  gcdmultiple  12157  nnwosdc  12176  alginv  12185  cncongr1  12241  prmdvdsexp  12286  prmndvdsfaclt  12294  dfgrp2  13099  srgmulgass  13485  lmodvsmmulgdi  13819  lmodfopnelem1  13820  rmodislmodlem  13846  cnfldmulg  14064  cnfldexp  14065  clsss  14286  xmettri2  14529  mettri  14541  metss  14662  zabsle1  15115  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem3  15179  gausslemma2dlem4  15180  bdssexg  15396  bj-findis  15471  nninfalllem1  15498  nninfsellemdc  15500  redc0  15547