Theorem 3expib 1122

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 1119	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

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

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 1088

This theorem is referenced by:  3anidm12  1421  mob  3691  dfss2  3935  eqbrrdva  5836  f1oiso2  7330  frxp  8108  onfununi  8313  smoel2  8335  smoiso2  8341  3ecoptocl  8785  ssfi  9143  f1domfi  9151  rex2dom  9200  fodomfib  9287  dffi2  9381  elfiun  9388  dif1card  9970  infxpenlem  9973  cfeq0  10216  cfsuc  10217  cfflb  10219  cfslb2n  10228  cofsmo  10229  domtriomlem  10402  axdc3lem4  10413  axdc4lem  10415  ttukey2g  10476  tskxpss  10732  grudomon  10777  elnpi  10948  dedekind  11344  nn0n0n1ge2b  12518  fzind  12639  suprzcl2  12904  icoshft  13441  fzen  13509  hashgt23el  14396  hashfundm  14414  hashbclem  14424  seqcoll  14436  relexpsucl  15004  relexpsucr  15005  relexpfld  15022  shftuz  15042  mulgcd  16525  algcvga  16556  lcmneg  16580  ressbas  17213  resseqnbas  17219  ressress  17224  psss  18546  tsrlemax  18552  isnmgm  18578  gsummgmpropd  18615  issgrpd  18664  iscmnd  19731  ring1ne0  20215  unitmulclb  20297  isdrngd  20681  isdrngdOLD  20683  abvn0b  20752  issrngd  20771  rmodislmodlem  20842  rmodislmod  20843  isphld  21570  mpfaddcl  22019  mpfmulcl  22020  pf1addcl  22247  pf1mulcl  22248  fitop  22794  hausnei2  23247  ordtt1  23273  locfincmp  23420  basqtop  23605  filfi  23753  fgcl  23772  neifil  23774  filuni  23779  cnextcn  23961  prdsmet  24265  blssps  24319  blss  24320  metcnp3  24435  hlhil  25350  volsup2  25513  sincosq1sgn  26414  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  sinq12ge0  26424  bcmono  27195  n0cutlt  28256  iswlkg  29548  umgrwwlks2on  29894  clwlkclwwlkfo  29945  3cyclfrgrrn1  30221  grpodivf  30474  ipf  30649  shintcli  31265  spanuni  31480  adjadj  31872  unopadj2  31874  hmopadj  31875  hmopbdoptHIL  31924  resvsca  33311  resvlem  33312  submateq  33806  esumcocn  34077  bnj1379  34827  bnj571  34903  bnj594  34909  bnj580  34910  bnj600  34916  bnj1189  35006  bnj1321  35024  bnj1384  35029  f1resrcmplf1dlem  35083  cplgredgex  35115  cusgr3cyclex  35130  loop1cycl  35131  umgr2cycllem  35134  umgr2cycl  35135  acycgr2v  35144  cusgracyclt3v  35150  climuzcnv  35665  fness  36344  bj-idreseq  37157  bj-imdiridlem  37180  neificl  37754  metf1o  37756  isismty  37802  ismtybndlem  37807  ablo4pnp  37881  divrngcl  37958  keridl  38033  prnc  38068  lsmsatcv  39010  llncvrlpln2  39558  lplncvrlvol2  39616  linepsubN  39753  pmapsub  39769  dalawlem10  39881  dalawlem13  39884  dalawlem14  39885  dalaw  39887  diaf11N  41050  dibf11N  41162  ismrcd1  42693  ismrcd2  42694  mzpincl  42729  mzpadd  42733  mzpmul  42734  pellfundge  42877  imasgim  43096  sqrtcval  43637  stoweidlem2  46007  stoweidlem17  46022  imaelsetpreimafv  47400  opnneir  48899  i0oii  48912  io1ii  48913