Theorem 3expib 1123

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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  df-3an 1089

This theorem is referenced by:  3anidm12  1422  mob  3664  dfss2  3908  eqbrrdva  5818  f1oiso2  7300  frxp  8069  onfununi  8274  smoel2  8296  smoiso2  8302  3ecoptocl  8749  ssfi  9100  f1domfi  9108  rex2dom  9156  fodomfib  9232  dffi2  9329  elfiun  9336  dif1card  9923  infxpenlem  9926  cfeq0  10169  cfsuc  10170  cfflb  10172  cfslb2n  10181  cofsmo  10182  domtriomlem  10355  axdc3lem4  10366  axdc4lem  10368  ttukey2g  10429  tskxpss  10686  grudomon  10731  elnpi  10902  dedekind  11300  nn0n0n1ge2b  12497  fzind  12618  suprzcl2  12879  icoshft  13417  fzen  13486  hashgt23el  14377  hashfundm  14395  hashbclem  14405  seqcoll  14417  relexpsucl  14984  relexpsucr  14985  relexpfld  15002  shftuz  15022  mulgcd  16508  algcvga  16539  lcmneg  16563  ressbas  17197  resseqnbas  17203  ressress  17208  psss  18537  tsrlemax  18543  isnmgm  18603  gsummgmpropd  18640  issgrpd  18689  iscmnd  19760  ring1ne0  20271  unitmulclb  20352  isdrngd  20733  isdrngdOLD  20735  abvn0b  20804  issrngd  20823  rmodislmodlem  20915  rmodislmod  20916  isphld  21644  mpfaddcl  22101  mpfmulcl  22102  pf1addcl  22328  pf1mulcl  22329  fitop  22875  hausnei2  23328  ordtt1  23354  locfincmp  23501  basqtop  23686  filfi  23834  fgcl  23853  neifil  23855  filuni  23860  cnextcn  24042  prdsmet  24345  blssps  24399  blss  24400  metcnp3  24515  hlhil  25420  volsup2  25582  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12ge0  26485  bcmono  27254  n0cutlt  28365  bdayfin  28493  iswlkg  29697  usgrwwlks2on  30041  umgrwwlks2on  30042  clwlkclwwlkfo  30094  3cyclfrgrrn1  30370  grpodivf  30624  ipf  30799  shintcli  31415  spanuni  31630  adjadj  32022  unopadj2  32024  hmopadj  32025  hmopbdoptHIL  32074  resvsca  33407  resvlem  33408  submateq  33969  esumcocn  34240  bnj1379  34988  bnj571  35064  bnj594  35070  bnj580  35071  bnj600  35077  bnj1189  35167  bnj1321  35185  bnj1384  35190  f1resrcmplf1dlem  35245  trssfir1om  35271  fineqvinfep  35285  trssfir1omregs  35296  cplgredgex  35319  cusgr3cyclex  35334  loop1cycl  35335  umgr2cycllem  35338  umgr2cycl  35339  acycgr2v  35348  cusgracyclt3v  35354  climuzcnv  35869  fness  36547  cgsex2gd  37467  bj-idreseq  37492  bj-imdiridlem  37515  neificl  38088  metf1o  38090  isismty  38136  ismtybndlem  38141  ablo4pnp  38215  divrngcl  38292  keridl  38367  prnc  38402  lsmsatcv  39470  llncvrlpln2  40017  lplncvrlvol2  40075  linepsubN  40212  pmapsub  40228  dalawlem10  40340  dalawlem13  40343  dalawlem14  40344  dalaw  40346  diaf11N  41509  dibf11N  41621  ismrcd1  43144  ismrcd2  43145  mzpincl  43180  mzpadd  43184  mzpmul  43185  pellfundge  43328  imasgim  43546  sqrtcval  44086  stoweidlem2  46448  stoweidlem17  46463  imaelsetpreimafv  47867  opnneir  49394  i0oii  49407  io1ii  49408