Theorem impexp 455

Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Assertion

Ref	Expression
impexp	⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		pm3.3 453	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 454	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 212	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  imdistan  577  pm4.14  818  nan  842  pm4.87  856  pm5.6  1017  2sb6  2120  r2allem  3153  r3al  3203  r19.23t  3261  ceqsralt  3489  rspc2gv  3592  ralrab  3658  ralrab2  3662  euind  3688  reu2  3689  reu3  3691  rmo4  3694  rmo3f  3698  reuind  3717  2reu5lem3  3721  rmo2  3841  rmo3  3843  rmoanim  3849  rmoanimALT  3850  ralss  4011  ralssOLD  4013  rabss  4025  raldifb  4104  ralin  4203  rabsssn  4635  raldifsni  4764  unissb  4907  elintrab  4926  ssintrab  4937  dftr5  5223  axrep5  5247  reusv2lem4  5374  reusv2  5376  reusv3  5378  raliunxp  5827  dfpo2  6299  fununi  6613  fvn0ssdmfun  7071  dff13  7254  ordunisuc2  7841  dfom2  7865  frpoins3xpg  8137  frpoins3xp3g  8138  xpord2indlem  8144  xpord3inddlem  8151  dfsmo2  8335  qliftfun  8801  dfsup2  9405  wemapsolem  9513  iscard2  9963  acnnum  10037  aceq1  10102  dfac9  10121  dfacacn  10126  axgroth6  10814  sstskm  10828  infm3  12175  prime  12678  raluz  12921  raluz2  12922  nnwos  12940  ralrp  13039  facwordi  14327  cotr2g  15015  rexuzre  15406  limsupgle  15530  ello12  15569  elo12  15580  lo1resb  15617  rlimresb  15618  o1resb  15619  modfsummod  15848  isprm2  16741  isprm4  16743  isprm7  16768  acsfn2  17720  pgpfac1  20153  isirred2  20504  isdomn3  20800  islindf4  21969  coe1fzgsumd  22445  evl1gsumd  22498  ist1-2  23485  isnrm2  23496  dfconn2  23557  1stccn  23601  iskgen3  23687  hausdiag  23783  cnflf  24140  txflf  24144  cnfcf  24180  metcnp  24679  caucfil  25423  ovolgelb  25620  ismbl  25666  dyadmbllem  25739  itg2leub  25874  ellimc3  26019  mdegleb  26202  jensen  27134  dchrelbas2  27382  dchrelbas3  27383  eqcuts2  27960  onsis  28448  ons2ind  28449  nmoubi  31105  nmobndseqi  31112  nmobndseqiALT  31113  h1dei  31883  nmopub  32241  nmfnleub  32258  mdsl1i  32654  mdsl2i  32655  elat2  32673  rabsspr  32828  rabsstp  32829  islinds5  33663  islbs5  33674  eulerpartlemgvv  34747  bnj115  35095  bnj1109  35156  bnj1533  35221  bnj580  35282  bnj864  35291  bnj865  35292  bnj1049  35343  bnj1090  35348  bnj1093  35349  bnj1133  35358  bnj1171  35369  climuzcnv  36144  axextprim  36174  biimpexp  36190  dfon2lem8  36261  dffun10  36385  filnetlem4  36873  mh-unprimbi  37036  bj-substax12  37330  wl-2sb6d  38194  poimirlem25  38277  poimirlem30  38282  r2alan  38881  inxpss  38947  moantr  39002  qmapeldisjsim  39490  isat3  40062  isltrn2N  40875  cdlemefrs29bpre0  41151  cdleme32fva  41192  sn-axrep5v  42969  dford4  43739  fnwe2lem2  43761  ifpidg  44200  ifpim23g  44204  elmapintrab  44285  undmrnresiss  44313  df3or2  44477  df3an2  44478  dfhe3  44484  dffrege76  44648  dffrege115  44687  ntrneiiso  44800  ismnushort  44994  pm11.62  45087  2sbc6g  45108  expcomdg  45192  impexpd  45205  dfvd2  45271  dfvd3  45283  modelac8prim  45684  rabssf  45820  2rexsb  47821  2rexrsb  47822  snlindsntor  49234  elbigo2  49315  exp12bd  49557  ralbidb  49561  ralbidc  49562  dfrals2  50551