Theorem expcom 115

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

Hypothesis

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

Assertion

Ref	Expression
expcom	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 114	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 30	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ancoms  266  syldan  280  sylan  281  animpimp2impd  548  pm4.79dc  888  dedlema  953  dedlemb  954  19.35-1  1603  cbval2  1893  cbvex2  1894  nelelne  2400  r19.21be  2523  r19.35-1  2581  mosubt  2861  sbcrext  2986  uneqdifeqim  3448  ssuni  3758  uniss2  3767  elpwuni  3902  elssabg  4073  elpw2g  4081  epelg  4212  elnn  4519  relop  4689  riinint  4800  cnviinm  5080  funopg  5157  fun  5295  tz6.12c  5451  fvelrnb  5469  fmptco  5586  fnressn  5606  fressnfv  5607  fvtp2g  5629  fvtp3g  5630  fconst2g  5635  isores3  5716  isoselem  5721  eloprabga  5858  fo1stresm  6059  poxp  6129  brtpos2  6148  smores  6189  tfrlem1  6205  tfrlemi1  6229  tfr1onlemaccex  6245  tfrcllemaccex  6258  frecrdg  6305  oawordriexmid  6366  nnacl  6376  nnmcl  6377  nnacom  6380  nnaass  6381  nnmsucr  6384  nndifsnid  6403  nnmordi  6412  iinerm  6501  th3qlem2  6532  elpmg  6558  pmss12g  6569  mapsn  6584  brdomg  6642  f1domg  6652  ssdomg  6672  nndomo  6758  elfi2  6860  carden2bex  7045  addclpi  7135  addnidpig  7144  genpassl  7332  genpassu  7333  nqprloc  7353  ltaprlem  7426  recexprlemopl  7433  recexprlemopu  7435  recexprlemupu  7436  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemupu  7457  caucvgprlemupu  7480  caucvgprprlemupu  7508  archsr  7590  peano2nnnn  7661  receuap  8430  peano2nn  8732  nnaddcl  8740  zrevaddcl  9104  nzadd  9106  zdiv  9139  nneo  9154  zeo2  9157  peano5uzti  9159  fzind  9166  fnn0ind  9167  lbzbi  9408  qrevaddcl  9436  irradd  9438  irrmul  9439  ltsubrp  9478  ltaddrp  9479  xnn0xadd0  9650  icoshft  9773  fzen  9823  elfzm11  9871  uzsplit  9872  fzoval  9925  elfzom1elp1fzo  9979  exfzdc  10017  modaddmodup  10160  frec2uzrdg  10182  seq3clss  10240  monoord  10249  seq3caopr3  10254  seq3f1olemp  10275  seq3id3  10280  seq3homo  10283  seq3z  10284  ser3ge0  10290  expadd  10335  expmul  10338  leexp1a  10348  faccl  10481  facdiv  10484  faclbnd  10487  faclbnd6  10490  omgadd  10548  hashunsng  10553  seq3coll  10585  shftlem  10588  resqrexlemover  10782  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc3  10788  climub  11113  climserle  11114  fsumzcl2  11174  fsumsplitsnun  11188  fsum2d  11204  modfsummodlemstep  11226  fsumabs  11234  fsumiun  11246  bcxmas  11258  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  prodfap0  11314  prodfrecap  11315  ntrivcvgap  11317  prodmodc  11347  dvds2ln  11526  dvdsabseq  11545  dvdsdivcl  11548  alzdvds  11552  oddnn02np1  11577  m1exp1  11598  nn0o1gt2  11602  nno  11603  ndvdsadd  11628  flodddiv4  11631  gcddiv  11707  gcdmultiple  11708  gcdmultiplez  11709  rplpwr  11715  dvdssq  11719  nn0seqcvgd  11722  alginv  11728  algcvga  11732  algfx  11733  isprm2  11798  isprm3  11799  prmdvdsexp  11826  ennnfoneleminc  11924  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemhom  11928  setsn0fun  11996  restopnb  12350  restdis  12353  tgcnp  12378  cnntr  12394  cnsscnp  12398  txcn  12444  txlm  12448  mettri  12542  blssexps  12598  blssex  12599  mopni3  12653  metss  12663  2spim  12973