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  549  pm4.79dc  889  dedlema  954  dedlemb  955  19.35-1  1604  cbval2  1894  cbvex2  1895  nelelne  2401  r19.21be  2526  r19.35-1  2584  mosubt  2865  sbcrext  2990  uneqdifeqim  3453  ssuni  3766  uniss2  3775  elpwuni  3910  elssabg  4081  elpw2g  4089  epelg  4220  elnn  4527  relop  4697  riinint  4808  cnviinm  5088  funopg  5165  fun  5303  tz6.12c  5459  fvelrnb  5477  fmptco  5594  fnressn  5614  fressnfv  5615  fvtp2g  5637  fvtp3g  5638  fconst2g  5643  isores3  5724  isoselem  5729  eloprabga  5866  fo1stresm  6067  poxp  6137  brtpos2  6156  smores  6197  tfrlem1  6213  tfrlemi1  6237  tfr1onlemaccex  6253  tfrcllemaccex  6266  frecrdg  6313  oawordriexmid  6374  nnacl  6384  nnmcl  6385  nnacom  6388  nnaass  6389  nnmsucr  6392  nndifsnid  6411  nnmordi  6420  iinerm  6509  th3qlem2  6540  elpmg  6566  pmss12g  6577  mapsn  6592  brdomg  6650  f1domg  6660  ssdomg  6680  nndomo  6766  elfi2  6868  carden2bex  7062  cc3  7100  addclpi  7159  addnidpig  7168  genpassl  7356  genpassu  7357  nqprloc  7377  ltaprlem  7450  recexprlemopl  7457  recexprlemopu  7459  recexprlemupu  7460  recexprlemss1l  7467  recexprlemss1u  7468  cauappcvgprlemupu  7481  caucvgprlemupu  7504  caucvgprprlemupu  7532  archsr  7614  peano2nnnn  7685  receuap  8454  peano2nn  8756  nnaddcl  8764  zrevaddcl  9128  nzadd  9130  zdiv  9163  nneo  9178  zeo2  9181  peano5uzti  9183  fzind  9190  fnn0ind  9191  lbzbi  9435  qrevaddcl  9463  irradd  9465  irrmul  9466  ltsubrp  9507  ltaddrp  9508  xnn0xadd0  9680  icoshft  9803  fzen  9854  elfzm11  9902  uzsplit  9903  fzoval  9956  elfzom1elp1fzo  10010  exfzdc  10048  modaddmodup  10191  frec2uzrdg  10213  seq3clss  10271  monoord  10280  seq3caopr3  10285  seq3f1olemp  10306  seq3id3  10311  seq3homo  10314  seq3z  10315  ser3ge0  10321  expadd  10366  expmul  10369  leexp1a  10379  faccl  10513  facdiv  10516  faclbnd  10519  faclbnd6  10522  omgadd  10580  hashunsng  10585  seq3coll  10617  shftlem  10620  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc3  10820  climub  11145  climserle  11146  fsumzcl2  11206  fsumsplitsnun  11220  fsum2d  11236  modfsummodlemstep  11258  fsumabs  11266  fsumiun  11278  bcxmas  11290  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  prodfap0  11346  prodfrecap  11347  ntrivcvgap  11349  prodmodc  11379  dvds2ln  11562  dvdsabseq  11581  dvdsdivcl  11584  alzdvds  11588  oddnn02np1  11613  m1exp1  11634  nn0o1gt2  11638  nno  11639  ndvdsadd  11664  flodddiv4  11667  gcddiv  11743  gcdmultiple  11744  gcdmultiplez  11745  rplpwr  11751  dvdssq  11755  nn0seqcvgd  11758  alginv  11764  algcvga  11768  algfx  11769  isprm2  11834  isprm3  11835  prmdvdsexp  11862  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemhom  11964  omiunct  11993  setsn0fun  12035  restopnb  12389  restdis  12392  tgcnp  12417  cnntr  12433  cnsscnp  12437  txcn  12483  txlm  12487  mettri  12581  blssexps  12637  blssex  12638  mopni3  12692  metss  12702  2spim  13144