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 208	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  imdistan  567  pm4.14  803  nan  826  pm4.87  839  pm5.6  998  2sb6  2090  r2allem  3123  r3al  3125  r19.23t  3241  moel  3349  ceqsralt  3453  rspc2gv  3561  ralrab  3623  ralrab2  3629  euind  3654  reu2  3655  reu3  3657  rmo4  3660  rmo3f  3664  reuind  3683  2reu5lem3  3687  rmo2  3816  rmo3  3818  rmoanim  3823  rmoanimALT  3824  ralss  3987  rabss  4001  raldifb  4075  rabsssn  4600  raldifsni  4725  unissb  4870  elintrab  4888  ssintrab  4899  dftr5  5190  axrep5  5211  reusv2lem4  5319  reusv2  5321  reusv3  5323  raliunxp  5737  dfpo2  6188  fununi  6493  fvn0ssdmfun  6934  dff13  7109  ordunisuc2  7666  dfom2  7689  dfsmo2  8149  qliftfun  8549  dfsup2  9133  wemapsolem  9239  iscard2  9665  acnnum  9739  aceq1  9804  dfac9  9823  dfacacn  9828  axgroth6  10515  sstskm  10529  infm3  11864  prime  12331  raluz  12565  raluz2  12566  nnwos  12584  ralrp  12679  facwordi  13931  cotr2g  14615  rexuzre  14992  limsupgle  15114  ello12  15153  elo12  15164  lo1resb  15201  rlimresb  15202  o1resb  15203  modfsummod  15434  isprm2  16315  isprm4  16317  isprm7  16341  acsfn2  17289  pgpfac1  19598  isirred2  19858  isdomn2  20483  islindf4  20955  coe1fzgsumd  21383  evl1gsumd  21433  ist1-2  22406  isnrm2  22417  dfconn2  22478  1stccn  22522  iskgen3  22608  hausdiag  22704  cnflf  23061  txflf  23065  cnfcf  23101  metcnp  23603  caucfil  24352  ovolgelb  24549  ismbl  24595  dyadmbllem  24668  itg2leub  24804  ellimc3  24948  mdegleb  25134  jensen  26043  dchrelbas2  26290  dchrelbas3  26291  nmoubi  29035  nmobndseqi  29042  nmobndseqiALT  29043  h1dei  29813  nmopub  30171  nmfnleub  30188  mdsl1i  30584  mdsl2i  30585  elat2  30603  islinds5  31465  eulerpartlemgvv  32243  bnj115  32604  bnj1109  32666  bnj1533  32732  bnj580  32793  bnj864  32802  bnj865  32803  bnj1049  32854  bnj1090  32859  bnj1093  32860  bnj1133  32869  bnj1171  32880  climuzcnv  33529  axextprim  33542  biimpexp  33561  dfon2lem8  33672  frpoins3xpg  33714  frpoins3xp3g  33715  xpord2ind  33721  xpord3ind  33727  eqscut2  33927  dffun10  34143  filnetlem4  34497  bj-substax12  34830  wl-2sb6d  35640  poimirlem25  35729  poimirlem30  35734  inxpss  36374  moantr  36421  isat3  37248  isltrn2N  38061  cdlemefrs29bpre0  38337  cdleme32fva  38378  sn-axrep5v  40113  dford4  40767  fnwe2lem2  40792  isdomn3  40945  ifpidg  40996  ifpim23g  41000  elmapintrab  41073  undmrnresiss  41101  df3or2  41265  df3an2  41266  dfhe3  41272  dffrege76  41436  dffrege115  41475  ntrneiiso  41590  ismnushort  41808  pm11.62  41901  2sbc6g  41922  expcomdg  42009  impexpd  42022  dfvd2  42088  dfvd3  42100  rabssf  42557  2rexsb  44480  2rexrsb  44481  snlindsntor  45700  elbigo2  45786  exp12bd  46029  ralbidb  46033  ralbidc  46034