Theorem impexp 451

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  imdistan  568  pm4.14  804  nan  827  pm4.87  840  pm5.6  999  2sb6  2089  r2allem  3117  r3al  3119  r19.23t  3246  moel  3358  moelOLD  3359  ceqsralt  3463  rspc2gv  3569  ralrab  3630  ralrab2  3635  euind  3659  reu2  3660  reu3  3662  rmo4  3665  rmo3f  3669  reuind  3688  2reu5lem3  3692  rmo2  3820  rmo3  3822  rmoanim  3827  rmoanimALT  3828  ralss  3991  rabss  4005  raldifb  4079  rabsssn  4603  raldifsni  4728  unissb  4873  elintrab  4891  ssintrab  4902  dftr5  5194  axrep5  5215  reusv2lem4  5324  reusv2  5326  reusv3  5328  raliunxp  5748  dfpo2  6199  fununi  6509  fvn0ssdmfun  6952  dff13  7128  ordunisuc2  7691  dfom2  7714  dfsmo2  8178  qliftfun  8591  dfsup2  9203  wemapsolem  9309  iscard2  9734  acnnum  9808  aceq1  9873  dfac9  9892  dfacacn  9897  axgroth6  10584  sstskm  10598  infm3  11934  prime  12401  raluz  12636  raluz2  12637  nnwos  12655  ralrp  12750  facwordi  14003  cotr2g  14687  rexuzre  15064  limsupgle  15186  ello12  15225  elo12  15236  lo1resb  15273  rlimresb  15274  o1resb  15275  modfsummod  15506  isprm2  16387  isprm4  16389  isprm7  16413  acsfn2  17372  pgpfac1  19683  isirred2  19943  isdomn2  20570  islindf4  21045  coe1fzgsumd  21473  evl1gsumd  21523  ist1-2  22498  isnrm2  22509  dfconn2  22570  1stccn  22614  iskgen3  22700  hausdiag  22796  cnflf  23153  txflf  23157  cnfcf  23193  metcnp  23697  caucfil  24447  ovolgelb  24644  ismbl  24690  dyadmbllem  24763  itg2leub  24899  ellimc3  25043  mdegleb  25229  jensen  26138  dchrelbas2  26385  dchrelbas3  26386  nmoubi  29134  nmobndseqi  29141  nmobndseqiALT  29142  h1dei  29912  nmopub  30270  nmfnleub  30287  mdsl1i  30683  mdsl2i  30684  elat2  30702  islinds5  31563  eulerpartlemgvv  32343  bnj115  32704  bnj1109  32766  bnj1533  32832  bnj580  32893  bnj864  32902  bnj865  32903  bnj1049  32954  bnj1090  32959  bnj1093  32960  bnj1133  32969  bnj1171  32980  climuzcnv  33629  axextprim  33642  biimpexp  33659  dfon2lem8  33766  frpoins3xpg  33787  frpoins3xp3g  33788  xpord2ind  33794  xpord3ind  33800  eqscut2  34000  dffun10  34216  filnetlem4  34570  bj-substax12  34903  wl-2sb6d  35713  poimirlem25  35802  poimirlem30  35807  inxpss  36447  moantr  36494  isat3  37321  isltrn2N  38134  cdlemefrs29bpre0  38410  cdleme32fva  38451  sn-axrep5v  40185  dford4  40851  fnwe2lem2  40876  isdomn3  41029  ifpidg  41098  ifpim23g  41102  elmapintrab  41184  undmrnresiss  41212  df3or2  41376  df3an2  41377  dfhe3  41383  dffrege76  41547  dffrege115  41586  ntrneiiso  41701  ismnushort  41919  pm11.62  42012  2sbc6g  42033  expcomdg  42120  impexpd  42133  dfvd2  42199  dfvd3  42211  rabssf  42668  2rexsb  44593  2rexrsb  44594  snlindsntor  45812  elbigo2  45898  exp12bd  46141  ralbidb  46145  ralbidc  46146