Theorem impexp 450

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 448	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 449	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 209	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imdistan  567  pm4.14  806  nan  829  pm4.87  842  pm5.6  1002  2sb6  2086  r2allem  3148  r3al  3203  r19.23t  3261  moelOLD  3413  ceqsralt  3524  rspc2gv  3645  ralrab  3715  ralrab2  3720  euind  3746  reu2  3747  reu3  3749  rmo4  3752  rmo3f  3756  reuind  3775  2reu5lem3  3779  rmo2  3909  rmo3  3911  rmoanim  3916  rmoanimALT  3917  ralss  4083  rabss  4095  raldifb  4172  rabsssn  4690  raldifsni  4820  unissb  4963  unissbOLD  4964  elintrab  4984  ssintrab  4995  dftr5  5287  dftr5OLD  5288  axrep5  5309  reusv2lem4  5419  reusv2  5421  reusv3  5423  raliunxp  5864  dfpo2  6327  fununi  6653  fvn0ssdmfun  7108  dff13  7292  ordunisuc2  7881  dfom2  7905  frpoins3xpg  8181  frpoins3xp3g  8182  xpord2indlem  8188  xpord3inddlem  8195  dfsmo2  8403  qliftfun  8860  dfsup2  9513  wemapsolem  9619  iscard2  10045  acnnum  10121  aceq1  10186  dfac9  10206  dfacacn  10211  axgroth6  10897  sstskm  10911  infm3  12254  prime  12724  raluz  12961  raluz2  12962  nnwos  12980  ralrp  13077  facwordi  14338  cotr2g  15025  rexuzre  15401  limsupgle  15523  ello12  15562  elo12  15573  lo1resb  15610  rlimresb  15611  o1resb  15612  modfsummod  15842  isprm2  16729  isprm4  16731  isprm7  16755  acsfn2  17721  pgpfac1  20124  isirred2  20447  isdomn2OLD  20734  isdomn3  20737  islindf4  21881  coe1fzgsumd  22329  evl1gsumd  22382  ist1-2  23376  isnrm2  23387  dfconn2  23448  1stccn  23492  iskgen3  23578  hausdiag  23674  cnflf  24031  txflf  24035  cnfcf  24071  metcnp  24575  caucfil  25336  ovolgelb  25534  ismbl  25580  dyadmbllem  25653  itg2leub  25789  ellimc3  25934  mdegleb  26123  jensen  27050  dchrelbas2  27299  dchrelbas3  27300  eqscut2  27869  nmoubi  30804  nmobndseqi  30811  nmobndseqiALT  30812  h1dei  31582  nmopub  31940  nmfnleub  31957  mdsl1i  32353  mdsl2i  32354  elat2  32372  rabsspr  32529  rabsstp  32530  islinds5  33360  islbs5  33373  eulerpartlemgvv  34341  bnj115  34701  bnj1109  34762  bnj1533  34828  bnj580  34889  bnj864  34898  bnj865  34899  bnj1049  34950  bnj1090  34955  bnj1093  34956  bnj1133  34965  bnj1171  34976  climuzcnv  35639  axextprim  35663  biimpexp  35679  dfon2lem8  35754  dffun10  35878  filnetlem4  36347  bj-substax12  36687  wl-2sb6d  37512  poimirlem25  37605  poimirlem30  37610  ralin  38204  r2alan  38205  inxpss  38267  moantr  38320  isat3  39263  isltrn2N  40077  cdlemefrs29bpre0  40353  cdleme32fva  40394  sn-axrep5v  42209  dford4  42986  fnwe2lem2  43008  ifpidg  43453  ifpim23g  43457  elmapintrab  43538  undmrnresiss  43566  df3or2  43730  df3an2  43731  dfhe3  43737  dffrege76  43901  dffrege115  43940  ntrneiiso  44053  ismnushort  44270  pm11.62  44363  2sbc6g  44384  expcomdg  44471  impexpd  44484  dfvd2  44550  dfvd3  44562  rabssf  45021  2rexsb  47016  2rexrsb  47017  snlindsntor  48200  elbigo2  48286  exp12bd  48529  ralbidb  48533  ralbidc  48534