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  554  pm4.79dc  898  dedlema  964  dedlemb  965  19.35-1  1617  cbval2  1914  cbvex2  1915  nelelne  2432  r19.21be  2561  r19.35-1  2620  mosubt  2907  sbcrext  3032  uneqdifeqim  3499  ssuni  3816  uniss2  3825  elpwuni  3960  elssabg  4132  elpw2g  4140  epelg  4273  elomssom  4587  relop  4759  riinint  4870  cnviinm  5150  funopg  5230  fun  5368  tz6.12c  5524  fvelrnb  5542  fmptco  5659  fnressn  5679  fressnfv  5680  fvtp2g  5702  fvtp3g  5703  fconst2g  5708  isores3  5791  isoselem  5796  eloprabga  5937  fo1stresm  6137  poxp  6208  brtpos2  6227  smores  6268  tfrlem1  6284  tfrlemi1  6308  tfr1onlemaccex  6324  tfrcllemaccex  6337  frecrdg  6384  oawordriexmid  6446  nnacl  6456  nnmcl  6457  nnacom  6460  nnaass  6461  nnmsucr  6464  nndifsnid  6483  nnmordi  6492  iinerm  6581  th3qlem2  6612  elpmg  6638  pmss12g  6649  mapsn  6664  brdomg  6722  f1domg  6732  ssdomg  6752  nndomo  6838  elfi2  6945  nnnninfeq2  7101  carden2bex  7153  cc3  7217  addclpi  7276  addnidpig  7285  genpassl  7473  genpassu  7474  nqprloc  7494  ltaprlem  7567  recexprlemopl  7574  recexprlemopu  7576  recexprlemupu  7577  recexprlemss1l  7584  recexprlemss1u  7585  cauappcvgprlemupu  7598  caucvgprlemupu  7621  caucvgprprlemupu  7649  archsr  7731  peano2nnnn  7802  receuap  8574  peano2nn  8877  nnaddcl  8885  zrevaddcl  9249  nzadd  9251  zdiv  9287  nneo  9302  zeo2  9305  peano5uzti  9307  fzind  9314  fnn0ind  9315  lbzbi  9562  qrevaddcl  9590  irradd  9592  irrmul  9593  ltsubrp  9634  ltaddrp  9635  xnn0xadd0  9811  icoshft  9934  fzen  9986  elfzm11  10034  uzsplit  10035  fzoval  10091  elfzom1elp1fzo  10145  exfzdc  10183  modaddmodup  10330  frec2uzrdg  10352  seq3clss  10410  monoord  10419  seq3caopr3  10424  seq3f1olemp  10445  seq3id3  10450  seq3homo  10453  seq3z  10454  ser3ge0  10460  expadd  10505  expmul  10508  leexp1a  10518  modqexp  10589  faccl  10656  facdiv  10659  faclbnd  10662  faclbnd6  10665  omgadd  10724  hashunsng  10729  seq3coll  10764  shftlem  10767  resqrexlemover  10961  resqrexlemdecn  10963  resqrexlemlo  10964  resqrexlemcalc3  10967  climub  11294  climserle  11295  fsumzcl2  11355  fsumsplitsnun  11369  fsum2d  11385  modfsummodlemstep  11407  fsumabs  11415  fsumiun  11427  bcxmas  11439  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  prodfap0  11495  prodfrecap  11496  ntrivcvgap  11498  prodmodc  11528  fprodssdc  11540  fprodabs  11566  fprod2d  11573  dvdsmod0  11742  dvds2ln  11773  dvdsabseq  11794  dvdsdivcl  11797  alzdvds  11801  oddnn02np1  11826  m1exp1  11847  nn0o1gt2  11851  nno  11852  ndvdsadd  11877  flodddiv4  11880  gcddiv  11961  gcdmultiple  11962  gcdmultiplez  11963  rplpwr  11969  dvdssq  11973  nn0seqcvgd  11982  alginv  11988  algcvga  11992  algfx  11993  isprm2  12058  isprm3  12059  prmdvdsexp  12089  eulerthlemrprm  12170  eulerthlema  12171  pcmpt  12282  ennnfoneleminc  12353  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemhom  12357  omiunct  12386  nninfdclemlt  12393  setsn0fun  12440  mgmcl  12600  restopnb  12934  restdis  12937  tgcnp  12962  cnntr  12978  cnsscnp  12982  txcn  13028  txlm  13032  mettri  13126  blssexps  13182  blssex  13183  mopni3  13237  metss  13247  2spim  13760